I do have some of my own code that I was able to modify to investigate this.
Short answer
(1) is not a theorem of $\mathbf{KD4.2}$ since it is invalid on the frame
$F=(W,R)$ where $W=\{A,B,C\}$ and $R=\{(A,A),(B,A),(B,B),(B,C),(C,A)\}$,
and $F$ is serial, transitive and convergent.
(2) is a theorem of $\mathbf{K4}$, hence it is valid on all transitive frames.
However, since it was substantially weakened from a $\mathbf{K4}$ equivalent axiom,
it is valid on some non-transitive frames too.
Details
I use an algebraic-style notation which is intended to shorten the formulas,
reduce parentheses and also input formulas quickly into the computer.
Precedence is as follows:
- 'L' and 'M' for necessity and possibility
- '!' for negation
- '.' for conjunction (but typically omitted)
- '+' for disjunction
- '->' and '<->'
Note that in both your formulas (1) and (2) the right-hand of the outermost implication
is a conjunction, so we can split them into:
(1a) M( MpL(p->q) ) L( Mp->M(pq) ) -> M( MpL( p -> M( MpL(p->q) )+L( Mp->M(pq) ) ) )
(1b) M( MpL(p->q) ) L( Mp->M(pq) ) -> L( Mp -> M( pM( MpL(p->q) )L( Mp->M(pq) ) ) )
(2a) M( MpL(p->q) ) L( Mp->M(pq) ) -> M( MpL( p -> M( MpL(p->q) )+L( Mp->M(pq) ) ) )
(2b) M( MpL(p->q) ) L( Mp->M(pq) ) -> L( Mp -> M( p( M( MpL(p->q) )+L( Mp->M(pq) ) ) ) )
Hopefully I did not make translation mistakes. Then we have the following:
Formula (1a)
Testing formula "M(MpL(p->q))L(Mp->M(pq))->M(MpL(p->M(MpL(p->q))L(Mp->M(pq))))"
on frame {A(A)B(ABC)C(A)}
Valuation {p(C)q(C)} => formula invalid at B
Sub-formula | A B C
--------------------------------------------------------------|------
p | 0 0 1
q | 0 0 1
Mp | 0 1 0
(p->q) | 1 1 1
L(p->q) | 1 1 1
MpL(p->q) | 0 1 0
M(MpL(p->q)) | 0 1 0
pq | 0 0 1
M(pq) | 0 1 0
(Mp->M(pq)) | 1 1 1
L(Mp->M(pq)) | 1 1 1
M(MpL(p->q))L(Mp->M(pq)) | 0 1 0 left hand
(p->M(MpL(p->q))L(Mp->M(pq))) | 1 1 0
L(p->M(MpL(p->q))L(Mp->M(pq))) | 1 0 1
MpL(p->M(MpL(p->q))L(Mp->M(pq))) | 0 0 0
M(MpL(p->M(MpL(p->q))L(Mp->M(pq)))) | 0 0 0 right hand
M(MpL(p->q))L(Mp->M(pq))->M(MpL(p->M(MpL(p->q))L(Mp->M(pq)))) | 1 0 1 1a
Formula (1b)
Testing formula "M(MpL(p->q))L(Mp->M(pq))->L(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))"
on frame {A(A)B(ABC)C(A)}
Valuation {p(C)q(C)} => formula invalid at B
Sub-formula | A B C
--------------------------------------------------------------|------
p | 0 0 1
q | 0 0 1
Mp | 0 1 0
(p->q) | 1 1 1
L(p->q) | 1 1 1
MpL(p->q) | 0 1 0
M(MpL(p->q)) | 0 1 0
pq | 0 0 1
M(pq) | 0 1 0
(Mp->M(pq)) | 1 1 1
L(Mp->M(pq)) | 1 1 1
M(MpL(p->q))L(Mp->M(pq)) | 0 1 0 left hand
pM(MpL(p->q))L(Mp->M(pq)) | 0 0 0
M(pM(MpL(p->q))L(Mp->M(pq))) | 0 0 0
(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))) | 1 0 1
L(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))) | 1 0 1 right hand
M(MpL(p->q))L(Mp->M(pq))->L(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))) | 1 0 1 1b
Formula (2a)
( 1) p -> (Lq->pLq) PC
( 2) Mp -> M(Lq->pLq) (1) + M-monotony
( 3) Mp -> (LLq->M(pLq)) (2) + M-addition + PC
( 4) MpLLq -> M(pLq) (3) + PC
( 5) Lq -> LLq Axiom 4
( 6) MpLq -> MpLLq (5) + PC
( 7) MpLq -> M(pLq) (4),(6) + MP
( 8) Lq -> Mp+Lq PC
( 9) LLq -> L(Mp+Lq) (8) + L-monotony
(10) Lq -> L(Mp+Lq) (5),(9) + MP
(11) pLq -> pL(Mp+Lq) (10) + PC
(12) M(pLq) -> M( pL(Mp+Lq) ) (11) + M-monotony
(13) MpLq -> M( pL(Mp+Lq) ) (7),(12) + MP
(14) MpLr -> M( pL(Mp+Lr) ) (13) + US q/r
(15) M(qs)Lr -> M( qsL(M(qs)+Lr) ) (14) + US p/qs
(16) qsL(M(qs)+Lr) -> sL(M(qs)+Lr) PC
(17) M( qsL(M(qs)+Lr) ) -> M( sL(M(qs)+Lr) ) (16) + M-monotony
(18) M(qs)Lr -> M( sL(M(qs)+Lr) ) (15),(17) + MP
(19) M(qs)+Lr -> ( p->M(qs)+Lr ) PC
(20) L( M(qs)+Lr ) -> L( p->M(qs)+Lr ) (19) + L-monotony
(21) sL( M(qs)+Lr ) -> sL( p->M(qs)+Lr ) (20) + PC
(22) M( sL( M(qs)+Lr ) ) -> M( sL( p->M(qs)+Lr ) ) (21) + M-monotony
(23) M(qs)Lr -> M( sL( p->M(qs)+Lr ) ) (18),(22) + MP
(24) M(qMp)Lr -> M( MpL( p->M(qMp)+Lr ) ) (23) + US s/Mp
(25) 2a from (24) + US q/L(p->q), r/Mp->M(pq)
Formula (2b)
(26) Lq -> ( Mp->M(pLq) ) (7) + PC
(27) LLq -> L( Mp->M(pLq) ) (26) + L-monotony
(28) Lq -> L( Mp->M(pLq) ) (5),(27) + MP
(29) Lr -> L( Mp->M(pLr) ) (28) + US q/r
(30) ( Mp->M(pLr) ) -> ( Mp->M(ps)+M(pLr) ) PC
(31) ( Mp->M(pLr) ) -> ( Mp->M( p(s+Lr) ) ) (30) + M-addition
(32) L( Mp->M(pLr) ) -> L( Mp->M( p(s+Lr) ) ) (31) + L-monotony
(33) Lr -> L( Mp->M( p(s+Lr) ) ) (29),(32) + MP
(34) sLr -> L( Mp->M( p(s+Lr) ) ) (33) + PC
(35) 2b from 34 + US s/M(MpL(p->q)), r/Mp->M(pq)
In fact, by eliminating step 34 above we obtain a stronger formula:
(2b') L( Mp->M(pq) ) -> L( Mp->M( p( M( MpL(p->q) )+L( Mp->M(pq) ) ) ) )
And you can try to prove the following using similar methods:
(2a') M( MpL(p->q) ) -> M( MpL( p->M( MpL(p->q) )+L( Mp->M(pq) ) ) )
Please doublecheck all this. At some point my program was absolutely correct,
but I hacked into it many times since.