let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of N
for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of N; :: thesis: for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)
let F, G, H be pre-Macro of S; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

per cases ( F = Stop S or G = Stop S or ( F <> Stop S & G <> Stop S ) ) ;

suppose A1: F = Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

hence (F ';' G) ';' H = G ';' H by Th60
.= F ';' (G ';' H) by A1, Th60 ;
:: thesis: verum

end;

suppose A2: G = Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

hence (F ';' G) ';' H = F ';' H by Th59
.= F ';' (G ';' H) by A2, Th60 ;
:: thesis: verum

end;

suppose that A3: F <> Stop S and
A4: G <> Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

set X = { (il. S,k) where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } ;
A5: card ((F ';' G) ';' H) = ((card (F ';' G)) + (card H)) - 1 by Th52
.= ((((card F) + (card G)) - 1) + (card H)) - 1 by Th52
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A6: card (F ';' (G ';' H)) = ((card F) + (card (G ';' H))) - 1 by Th52
.= ((card F) + (((card G) + (card H)) - 1)) - 1 by Th52
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A7: dom ((F ';' G) ';' H) = { (il. S,k) where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } by A5, Th15;
A8: dom (F ';' (G ';' H)) = { (il. S,k) where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } by A6, Th15;
for x being set st x in { (il. S,k) where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } holds
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

proof

let x be set ; :: thesis: ( x in { (il. S,k) where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } implies ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x )
assume x in { (il. S,k) where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
then consider k being Element of NAT such that
A9: x = il. S,k and
A10: k < ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A11: dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr (G ';' H),((card F) -' 1)) } by Def16;
A12: dom (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) = { (il. S,(m + ((card (F ';' G)) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr H,((card (F ';' G)) -' 1)) } by Def16;
A13: dom (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1)) = { (il. S,(m + ((card G) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr H,((card G) -' 1)) } by Def16;
A14: (card (F ';' G)) -' 1 = (card (F ';' G)) - 1 by PRE_CIRC:25
.= (((card F) + (card G)) - 1) - 1 by Th52 ;
then (card (F ';' G)) -' 1 = ((card F) - 1) + ((card G) - 1) ;
then A15: (card (F ';' G)) -' 1 = ((card G) -' 1) + ((card F) - 1) by PRE_CIRC:25
.= ((card G) -' 1) + ((card F) -' 1) by PRE_CIRC:25 ;
A16: dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr G,((card F) -' 1)) } by Def16;
A17: (card F) -' 1 = (card F) - 1 by PRE_CIRC:25;
A18: (card G) -' 1 = (card G) - 1 by PRE_CIRC:25;
A19: for W being pre-Macro of S st W <> Stop S holds
2 <= card W

proof

let W be pre-Macro of S; :: thesis: ( W <> Stop S implies 2 <= card W )
assume A20: W <> Stop S ; :: thesis: 2 <= card W
assume 2 > card W ; :: thesis: contradiction
then 1 + 1 > card W ;
then card W <= 1 by NAT_1:13;
hence contradiction by A20, Th26, NAT_1:26; :: thesis: verum

end;

then 2 <= card F by A3;
then A21: 1 <= card F by XXREAL_0:2;
A22: 2 <= card G by A4, A19;

per cases ( k < (card F) - 1 or k = (card F) - 1 or ( card F <= k & k <= ((card F) + (card G)) - 3 ) or k = ((card F) + (card G)) - 2 or ((card F) + (card G)) - 2 < k ) by A21, A22, Lm2;

suppose A23: k < (card F) - 1 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

A24: CutLastLoc F c= CutLastLoc (F ';' G) by Th54;

A25: now

assume x in dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) ; :: thesis: contradiction
then consider m being Element of NAT such that
A26: x = il. S,(m + ((card F) -' 1)) and
il. S,m in dom (IncAddr (G ';' H),((card F) -' 1)) by A11;
k = m + ((card F) -' 1) by A9, A26, AMISTD_1:25
.= m + ((card F) - 1) by PRE_CIRC:25 ;
then m + ((card F) - 1) < (card F) -' 1 by A23, PRE_CIRC:25;
then m + ((card F) -' 1) < (card F) -' 1 by PRE_CIRC:25;
hence contradiction by NAT_1:11; :: thesis: verum

end;

A27: now

assume x in dom (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) ; :: thesis: contradiction
then consider m being Element of NAT such that
A28: x = il. S,(m + ((card (F ';' G)) -' 1)) and
il. S,m in dom (IncAddr H,((card (F ';' G)) -' 1)) by A12;
k = (m + ((card G) -' 1)) + ((card F) -' 1) by A9, A15, A28, AMISTD_1:25;
then (m + ((card G) -' 1)) + ((card F) -' 1) < (card F) -' 1 by A23, PRE_CIRC:25;
hence contradiction by NAT_1:11; :: thesis: verum

end;

k < card (CutLastLoc F) by A23, Th49;
then A29: x in dom (CutLastLoc F) by A9, AMISTD_1:50;
thus ((F ';' G) ';' H) . x = (CutLastLoc (F ';' G)) . x by A27, FUNCT_4:12
.= (CutLastLoc F) . x by A24, A29, GRFUNC_1:8
.= (F ';' (G ';' H)) . x by A25, FUNCT_4:12 ; :: thesis: verum

end;

suppose A30: k = (card F) - 1 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

A31: now

assume x in dom (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) ; :: thesis: contradiction
then consider m being Element of NAT such that
A32: x = il. S,(m + ((card (F ';' G)) -' 1)) and
il. S,m in dom (IncAddr H,((card (F ';' G)) -' 1)) by A12;
k = (m + ((card G) -' 1)) + ((card F) -' 1) by A9, A15, A32, AMISTD_1:25;
then (m + ((card G) -' 1)) + ((card F) -' 1) = (card F) -' 1 by A30, PRE_CIRC:25;
then (card G) -' 1 = 0 ;
then (card G) - 1 = 0 by PRE_CIRC:25;
hence contradiction by A4, Th26; :: thesis: verum

end;

A33: il. S,0 in dom (IncAddr (G ';' H),((card F) -' 1)) by AMISTD_1:49;
A34: il. S,0 in dom (IncAddr G,((card F) -' 1)) by AMISTD_1:49;
A35: il. S,0 in dom G by AMISTD_1:49;
A36: il. S,0 in dom (G ';' H) by AMISTD_1:49;
k = 0 + ((card F) -' 1) by A30, PRE_CIRC:25;
then A37: x in dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) by A9, A11, A33;
A38: k = (card F) -' 1 by A30, PRE_CIRC:25;
A39: x = il. S,(0 + k) by A9;
il. S,0 in dom (IncAddr G,((card F) -' 1)) by AMISTD_1:49;
then A40: x in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A16, A38, A39;
then x in (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by XBOOLE_0:def 3;
then A41: x in dom (F ';' G) by FUNCT_4:def 1;

now

A42: dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) = {(LastLoc (F ';' G))} by FUNCOP_1:19
.= {(il. S,((card (F ';' G)) -' 1))} by AMISTD_1:55 ;
assume x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; :: thesis: contradiction
then x = il. S,((card (F ';' G)) -' 1) by A42, TARSKI:def 1;
then k = ((card G) -' 1) + ((card F) -' 1) by A9, A15, AMISTD_1:25;
then (card G) - 1 = 0 by A38, PRE_CIRC:25;
hence contradiction by A4, Th26; :: thesis: verum

end;

then A43: x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A41, XBOOLE_0:def 5;
1 <= card G by NAT_1:14;
then card G > 1 by A4, Th26, XXREAL_0:1;
then A44: (card G) - 1 > 1 - 1 by XREAL_1:11;
then (card G) -' 1 > 1 - 1 by PRE_CIRC:25;
then A45: not il. S,0 in dom (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1)) by Th41;
card (CutLastLoc G) <> {} by A44, Th49;
then A46: il. S,0 in dom (CutLastLoc G) by AMISTD_1:49, CARD_1:47;
A47: pi G,(il. S,0 ) = G . (il. S,0 ) by A35, AMI_1:def 47
.= (CutLastLoc G) . (il. S,0 ) by A46, GRFUNC_1:8
.= (G ';' H) . (il. S,0 ) by A45, FUNCT_4:12
.= pi (G ';' H),(il. S,0 ) by A36, AMI_1:def 47 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A31, FUNCT_4:12
.= ((CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) . x by A43, GRFUNC_1:93
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . x by A40, FUNCT_4:14
.= (IncAddr G,((card F) -' 1)) . (il. S,0 ) by A34, A38, A39, Def16
.= IncAddr (pi (G ';' H),(il. S,0 )),((card F) -' 1) by A35, A47, Def15
.= (IncAddr (G ';' H),((card F) -' 1)) . (il. S,0 ) by A36, Def15
.= (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) . x by A33, A38, A39, Def16
.= (F ';' (G ';' H)) . x by A37, FUNCT_4:14 ; :: thesis: verum

end;

suppose that A48: card F <= k and
A49: k <= ((card F) + (card G)) - 3 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

A50: now

assume x in dom (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) ; :: thesis: contradiction
then consider m being Element of NAT such that
A51: x = il. S,(m + ((card (F ';' G)) -' 1)) and
il. S,m in dom (IncAddr H,((card (F ';' G)) -' 1)) by A12;
m + (((card G) -' 1) + ((card F) -' 1)) <= (- 1) + (((card G) -' 1) + ((card F) -' 1)) by A9, A15, A17, A18, A49, A51, AMISTD_1:25;
then m <= - 1 by XREAL_1:8;
hence contradiction by Lm1; :: thesis: verum

end;

(card F) -' 1 <= card F by NAT_D:35;
then A52: x = il. S,((k -' ((card F) -' 1)) + ((card F) -' 1)) by A9, A48, XREAL_1:237, XXREAL_0:2;
A53: (card F) - (card F) <= k - (card F) by A48, XREAL_1:11;
(card F) - 1 < (card F) - 0 by XREAL_1:17;
then k - ((card F) - 1) >= 0 by A53, XREAL_1:17;
then A54: k - ((card F) -' 1) >= 0 by PRE_CIRC:25;
A55: ((card F) + (card G)) - 3 < (((card F) + (card G)) - 3) + 1 by XREAL_1:31;
then A56: k < ((card G) - 1) + ((card F) - 1) by A49, XXREAL_0:2;
(k - ((card F) - 1)) + ((card F) - 1) < ((card G) - 1) + ((card F) - 1) by A49, A55, XXREAL_0:2;
then k - ((card F) - 1) < (card G) - 1 by XREAL_1:9;
then k - ((card F) -' 1) < (card G) - 1 by PRE_CIRC:25;
then k -' ((card F) -' 1) < (card G) - 1 by A54, XREAL_0:def 2;
then k -' ((card F) -' 1) < card (CutLastLoc G) by Th49;
then A57: il. S,(k -' ((card F) -' 1)) in dom (CutLastLoc G) by AMISTD_1:50;
then il. S,(k -' ((card F) -' 1)) in (dom (CutLastLoc G)) \/ (dom (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1))) by XBOOLE_0:def 3;
then A58: il. S,(k -' ((card F) -' 1)) in dom (G ';' H) by FUNCT_4:def 1;
then A59: il. S,(k -' ((card F) -' 1)) in dom (IncAddr (G ';' H),((card F) -' 1)) by Def15;
then A60: x in dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) by A11, A52;
((card G) + (card F)) - 2 < ((card F) + (card G)) - 1 by XREAL_1:17;
then k < ((card F) + (card G)) - 1 by A56, XXREAL_0:2;
then k < card (F ';' G) by Th52;
then A61: x in dom (F ';' G) by A9, AMISTD_1:50;

now

assume x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; :: thesis: contradiction
then x in {(LastLoc (F ';' G))} by FUNCOP_1:19;
then x = LastLoc (F ';' G) by TARSKI:def 1
.= il. S,((card (F ';' G)) -' 1) by AMISTD_1:55 ;
then k = (card (F ';' G)) -' 1 by A9, AMISTD_1:25
.= ((card G) - 1) + ((card F) - 1) by A15, A18, PRE_CIRC:25 ;
hence contradiction by A49, A55; :: thesis: verum

end;

then A62: x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A61, XBOOLE_0:def 5;
A63: dom (CutLastLoc G) c= dom G by GRFUNC_1:8;
then il. S,(k -' ((card F) -' 1)) in dom G by A57;
then A64: il. S,(k -' ((card F) -' 1)) in dom (IncAddr G,((card F) -' 1)) by Def15;
then A65: x in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A16, A52;

A66: now

assume il. S,(k -' ((card F) -' 1)) in dom (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1)) ; :: thesis: contradiction
then consider m being Element of NAT such that
A67: il. S,(k -' ((card F) -' 1)) = il. S,(m + ((card G) -' 1)) and
il. S,m in dom (IncAddr H,((card G) -' 1)) by A13;
k -' ((card F) -' 1) = m + ((card G) -' 1) by A67, AMISTD_1:25;
then A68: m = (k -' ((card F) -' 1)) - ((card G) -' 1)
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A54, XREAL_0:def 2
.= (k - ((card F) - 1)) - ((card G) -' 1) by PRE_CIRC:25
.= (k - ((card F) - 1)) - ((card G) - 1) by PRE_CIRC:25
.= k - (((card F) + (card G)) - 2) ;
k - (((card F) + (card G)) - 2) <= (((card F) + (card G)) - 3) - (((card F) + (card G)) - 2) by A49, XREAL_1:11;
hence contradiction by A68, Lm1; :: thesis: verum

end;

A69: pi (G ';' H),(il. S,(k -' ((card F) -' 1))) = ((CutLastLoc G) +* (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1))) . (il. S,(k -' ((card F) -' 1))) by A58, AMI_1:def 47
.= (CutLastLoc G) . (il. S,(k -' ((card F) -' 1))) by A66, FUNCT_4:12
.= G . (il. S,(k -' ((card F) -' 1))) by A57, GRFUNC_1:8 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A50, FUNCT_4:12
.= ((CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) . x by A62, GRFUNC_1:93
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . x by A65, FUNCT_4:14
.= (IncAddr G,((card F) -' 1)) . (il. S,(k -' ((card F) -' 1))) by A52, A64, Def16
.= IncAddr (pi G,(il. S,(k -' ((card F) -' 1)))),((card F) -' 1) by A57, A63, Def15
.= IncAddr (pi (G ';' H),(il. S,(k -' ((card F) -' 1)))),((card F) -' 1) by A57, A63, A69, AMI_1:def 47
.= (IncAddr (G ';' H),((card F) -' 1)) . (il. S,(k -' ((card F) -' 1))) by A58, Def15
.= (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) . x by A52, A59, Def16
.= (F ';' (G ';' H)) . x by A60, FUNCT_4:14 ; :: thesis: verum

end;

suppose A70: k = ((card F) + (card G)) - 2 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

then A71: x = il. S,((k -' ((card (F ';' G)) -' 1)) + ((card (F ';' G)) -' 1)) by A9, A14, XREAL_1:237;
k - ((card (F ';' G)) -' 1) = 0 by A14, A70;
then A72: k -' ((card (F ';' G)) -' 1) = 0 by XREAL_0:def 2;
then A73: il. S,(k -' ((card (F ';' G)) -' 1)) in dom (IncAddr H,((card (F ';' G)) -' 1)) by AMISTD_1:49;
then A74: x in dom (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) by A12, A71;
A75: x = il. S,(((card G) -' 1) + ((card F) -' 1)) by A9, A17, A18, A70;
((card G) - 1) + 0 < ((card G) - 1) + (card H) by XREAL_1:8;
then (card G) -' 1 < ((card G) + (card H)) - 1 by PRE_CIRC:25;
then (card G) -' 1 < card (G ';' H) by Th52;
then A76: il. S,((card G) -' 1) in dom (G ';' H) by AMISTD_1:50;
then A77: il. S,((card G) -' 1) in dom (IncAddr (G ';' H),((card F) -' 1)) by Def15;
then A78: x in dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) by A11, A75;
A79: il. S,0 in dom H by AMISTD_1:49;
A80: pi (G ';' H),(il. S,((card G) -' 1)) = (G ';' H) . (il. S,((card G) -' 1)) by A76, AMI_1:def 47;
A81: il. S,0 in dom (IncAddr H,((card G) -' 1)) by AMISTD_1:49;
then A82: pi (IncAddr H,((card G) -' 1)),(il. S,0 ) = (IncAddr H,((card G) -' 1)) . (il. S,0 ) by AMI_1:def 47
.= IncAddr (pi H,(il. S,0 )),((card G) -' 1) by A79, Def15 ;
pi (G ';' H),(il. S,((card G) -' 1)) = (G ';' H) . (LastLoc G) by A80, AMISTD_1:55
.= (IncAddr H,((card G) -' 1)) . (il. S,0 ) by Th55
.= pi (IncAddr H,((card G) -' 1)),(il. S,0 ) by A81, AMI_1:def 47 ;
then A83: IncAddr (pi (G ';' H),(il. S,((card G) -' 1))),((card F) -' 1) = IncAddr (pi H,(il. S,0 )),((card (F ';' G)) -' 1) by A15, A82, Th37;
thus ((F ';' G) ';' H) . x = (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) . x by A74, FUNCT_4:14
.= (IncAddr H,((card (F ';' G)) -' 1)) . (il. S,(k -' ((card (F ';' G)) -' 1))) by A71, A73, Def16
.= IncAddr (pi H,(il. S,0 )),((card (F ';' G)) -' 1) by A72, A79, Def15
.= (IncAddr (G ';' H),((card F) -' 1)) . (il. S,((card G) -' 1)) by A76, A83, Def15
.= (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) . x by A75, A77, Def16
.= (F ';' (G ';' H)) . x by A78, FUNCT_4:14 ; :: thesis: verum

end;

suppose A84: ((card F) + (card G)) - 2 < k ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

then A85: x = il. S,((k -' ((card (F ';' G)) -' 1)) + ((card (F ';' G)) -' 1)) by A9, A14, XREAL_1:237;
k + 0 < (((card F) + (card G)) - (1 + 1)) + (card H) by A10;
then k - (((card F) + (card G)) - (1 + 1)) < (card H) - 0 by XREAL_1:23;
then k -' ((card (F ';' G)) -' 1) < card H by A14, XREAL_0:def 2;
then A86: il. S,(k -' ((card (F ';' G)) -' 1)) in dom H by AMISTD_1:50;
then A87: il. S,(k -' ((card (F ';' G)) -' 1)) in dom (IncAddr H,((card (F ';' G)) -' 1)) by Def15;
then A88: x in dom (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) by A12, A85;
A89: (card F) -' 1 <= ((card G) -' 1) + ((card F) -' 1) by NAT_1:11;
then A90: k >= (card F) -' 1 by A14, A15, A84, XXREAL_0:2;
A91: x = il. S,((k -' ((card F) -' 1)) + ((card F) -' 1)) by A9, A14, A15, A84, A89, XREAL_1:237, XXREAL_0:2;
A92: k - ((card F) -' 1) >= 0 by A90, XREAL_1:50;
A93: k - ((card F) -' 1) < (((((card F) + (card G)) + (card H)) - 1) - 1) - ((card F) -' 1) by A10, XREAL_1:11;
then A94: k -' ((card F) -' 1) < ((((card F) + (card G)) + (card H)) - (card F)) - 1 by A17, A92, XREAL_0:def 2;
k -' ((card F) -' 1) < ((((card F) - (card F)) + (card G)) + (card H)) - 1 by A17, A92, A93, XREAL_0:def 2;
then k -' ((card F) -' 1) < card (G ';' H) by Th52;
then A95: il. S,(k -' ((card F) -' 1)) in dom (G ';' H) by AMISTD_1:50;
then il. S,(k -' ((card F) -' 1)) in dom (IncAddr (G ';' H),((card F) -' 1)) by Def15;
then A96: x in dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) by A11, A91;
A97: il. S,(k -' ((card F) -' 1)) in dom (IncAddr (G ';' H),((card F) -' 1)) by A95, Def15;
A98: k - ((card F) -' 1) >= ((card (F ';' G)) -' 1) - ((card F) -' 1) by A14, A84, XREAL_1:11;
then A99: k -' ((card F) -' 1) >= (((card F) -' 1) + ((card G) -' 1)) - ((card F) -' 1) by A14, A15, A84, A89, XREAL_1:235, XXREAL_0:2;
A100: k -' ((card F) -' 1) >= (card G) -' 1 by A14, A15, A84, A89, A98, XREAL_1:235, XXREAL_0:2;
A101: il. S,(k -' ((card F) -' 1)) = il. S,(((k -' ((card F) -' 1)) -' ((card G) -' 1)) + ((card G) -' 1)) by A99, XREAL_1:237;
(k -' ((card F) -' 1)) - ((card G) -' 1) < (((card G) + (card H)) - 1) - ((card G) - 1) by A18, A94, XREAL_1:11;
then (k -' ((card F) -' 1)) -' ((card G) -' 1) < ((card H) + ((card G) - 1)) - ((card G) - 1) by A100, XREAL_1:235;
then il. S,((k -' ((card F) -' 1)) -' ((card G) -' 1)) in dom H by AMISTD_1:50;
then A102: il. S,((k -' ((card F) -' 1)) -' ((card G) -' 1)) in dom (IncAddr H,((card G) -' 1)) by Def15;
then A103: il. S,(k -' ((card F) -' 1)) in dom (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1)) by A13, A101;
A104: (k -' ((card F) -' 1)) -' ((card G) -' 1) = (k -' ((card F) -' 1)) - ((card G) -' 1) by A99, XREAL_1:235
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A14, A15, A84, A89, XREAL_1:235, XXREAL_0:2
.= k - (((card F) -' 1) + ((card G) -' 1))
.= k -' ((card (F ';' G)) -' 1) by A14, A15, A84, XREAL_1:235 ;
A105: pi (G ';' H),(il. S,(k -' ((card F) -' 1))) = ((CutLastLoc G) +* (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1))) . (il. S,(k -' ((card F) -' 1))) by A95, AMI_1:def 47
.= (Shift (IncAddr H,((card G) -' 1)),((card G) -' 1)) . (il. S,(k -' ((card F) -' 1))) by A103, FUNCT_4:14
.= (IncAddr H,((card G) -' 1)) . (il. S,(k -' ((card (F ';' G)) -' 1))) by A101, A102, A104, Def16
.= IncAddr (pi H,(il. S,(k -' ((card (F ';' G)) -' 1)))),((card G) -' 1) by A86, Def15 ;
thus ((F ';' G) ';' H) . x = (Shift (IncAddr H,((card (F ';' G)) -' 1)),((card (F ';' G)) -' 1)) . x by A88, FUNCT_4:14
.= (IncAddr H,((card (F ';' G)) -' 1)) . (il. S,(k -' ((card (F ';' G)) -' 1))) by A85, A87, Def16
.= IncAddr (pi H,(il. S,(k -' ((card (F ';' G)) -' 1)))),((card (F ';' G)) -' 1) by A86, Def15
.= IncAddr (pi (G ';' H),(il. S,(k -' ((card F) -' 1)))),((card F) -' 1) by A15, A105, Th37
.= (IncAddr (G ';' H),((card F) -' 1)) . (il. S,(k -' ((card F) -' 1))) by A95, Def15
.= (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) . x by A91, A97, Def16
.= (F ';' (G ';' H)) . x by A96, FUNCT_4:14 ; :: thesis: verum

end;

end;

end;

hence (F ';' G) ';' H = F ';' (G ';' H) by A7, A8, FUNCT_1:9; :: thesis: verum

end;

end;