āf1,f2,L1,L2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦ ā
āg1,I,K1,X. f1 = āg1 ā L1 = K1.ā{I}X ā
āØāØ āāg2,K2. ā¦K1,g1ā¦ ā«š
+ ā¦K2,g2ā¦ & f2 = āg2 & L2 = K2.ā{I}X
āf1,f2,L1,L2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦ ā
āg1,I,K1,X. f1 = āg1 ā L1 = K1.ā{I}X ā
āØāØ āāg2,K2. ā¦K1,g1ā¦ ā«š
+ ā¦K2,g2ā¦ & f2 = āg2 & L2 = K2.ā{I}X