let N be 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 NAT ,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 NAT ,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 A22: 1 <= card F by XXREAL_0:2;
A23: 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 A22, A23, Lm2;

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

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

A26: 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
A27: 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, A27, AMISTD_1:25
.= m + ((card F) - 1) by PRE_CIRC:25 ;
then m + ((card F) - 1) < (card F) -' 1 by A24, PRE_CIRC:25;
then m + ((card F) -' 1) < (card F) -' 1 by PRE_CIRC:25;
hence contradiction by NAT_1:11; :: thesis: verum

end;

A28: 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
A29: 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, A29, AMISTD_1:25;
then (m + ((card G) -' 1)) + ((card F) -' 1) < (card F) -' 1 by A24, PRE_CIRC:25;
hence contradiction by NAT_1:11; :: thesis: verum

end;

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

end;

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

A32: 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
A33: 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, A33, AMISTD_1:25;
then (m + ((card G) -' 1)) + ((card F) -' 1) = (card F) -' 1 by A31, 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;

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

now

A43: 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 A43, TARSKI:def 1;
then k = ((card G) -' 1) + ((card F) -' 1) by A9, A15, AMISTD_1:25;
then (card G) - 1 = 0 by A39, PRE_CIRC:25;
hence contradiction by A4, Th26; :: thesis: verum

end;

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

end;

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

A51: 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
A52: 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, A50, A52, 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 A53: x = il. S,((k -' ((card F) -' 1)) + ((card F) -' 1)) by A9, A49, XREAL_1:237, XXREAL_0:2;
A54: (card F) - (card F) <= k - (card F) by A49, XREAL_1:11;
(card F) - 1 < (card F) - 0 by XREAL_1:17;
then k - ((card F) - 1) >= 0 by A54, XREAL_1:17;
then A55: k - ((card F) -' 1) >= 0 by PRE_CIRC:25;
A56: ((card F) + (card G)) - 3 < (((card F) + (card G)) - 3) + 1 by XREAL_1:31;
then A57: k < ((card G) - 1) + ((card F) - 1) by A50, XXREAL_0:2;
(k - ((card F) - 1)) + ((card F) - 1) < ((card G) - 1) + ((card F) - 1) by A50, A56, 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 A55, XREAL_0:def 2;
then k -' ((card F) -' 1) < card (CutLastLoc G) by Th49;
then A58: 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 A59: il. S,(k -' ((card F) -' 1)) in dom (G ';' H) by FUNCT_4:def 1;
then A60: il. S,(k -' ((card F) -' 1)) in dom (IncAddr (G ';' H),((card F) -' 1)) by Def15;
then A61: x in dom (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) by A11, A53;
((card G) + (card F)) - 2 < ((card F) + (card G)) - 1 by XREAL_1:17;
then k < ((card F) + (card G)) - 1 by A57, XXREAL_0:2;
then k < card (F ';' G) by Th52;
then A62: 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 A50, A56; :: thesis: verum

end;

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

A67: 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
A68: 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 A68, AMISTD_1:25;
then A69: m = (k -' ((card F) -' 1)) - ((card G) -' 1)
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A55, 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 A50, XREAL_1:11;
hence contradiction by A69, Lm1; :: thesis: verum

end;

A70: 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 A59, AMI_1:def 47
.= (CutLastLoc G) . (il. S,(k -' ((card F) -' 1))) by A67, FUNCT_4:12
.= G . (il. S,(k -' ((card F) -' 1))) by A58, GRFUNC_1:8 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A51, FUNCT_4:12
.= ((CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) . x by A63, GRFUNC_1:93
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . x by A66, FUNCT_4:14
.= (IncAddr G,((card F) -' 1)) . (il. S,(k -' ((card F) -' 1))) by A53, A65, Def16
.= IncAddr (pi G,(il. S,(k -' ((card F) -' 1)))),((card F) -' 1) by A58, A64, Def15
.= IncAddr (pi (G ';' H),(il. S,(k -' ((card F) -' 1)))),((card F) -' 1) by A58, A64, A70, AMI_1:def 47
.= (IncAddr (G ';' H),((card F) -' 1)) . (il. S,(k -' ((card F) -' 1))) by A59, Def15
.= (Shift (IncAddr (G ';' H),((card F) -' 1)),((card F) -' 1)) . x by A53, A60, Def16
.= (F ';' (G ';' H)) . x by A61, FUNCT_4:14 ; :: thesis: verum

end;

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

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

end;

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

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