set P = F ';' G;
set k = (card F) -' 1;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by FUNCT_4:def 1;
A2: 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;
A4: (card G) - 1 >= 0 by NAT_1:14, XREAL_1:50;
then ((card F) -' 1) + ((card G) - 1) >= ((card F) -' 1) + 0 by XREAL_1:8;
then A5: (((card F) -' 1) + (card G)) -' 1 = (((card F) -' 1) + (card G)) - 1 by XREAL_0:def 2
.= ((card F) -' 1) + ((card G) - 1)
.= ((card F) -' 1) + ((card G) -' 1) by A4, XREAL_0:def 2 ;
let f be Instruction-Location of S; :: according to AMISTD_1:def 23 :: thesis: ( not (F ';' G) . f = halt S or not f in dom (F ';' G) or f = LastLoc (F ';' G) )
assume that
A6: (F ';' G) . f = halt S and
A7: f in dom (F ';' G) ; :: thesis: f = LastLoc (F ';' G)

per cases ( f in dom (CutLastLoc F) or f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) ) by A1, A7, XBOOLE_0:def 3;

suppose A8: f in dom (CutLastLoc F) ; :: thesis: f = LastLoc (F ';' G)

then A9: (CutLastLoc F) . f <> halt S by Th51;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by Th50;
then CutLastLoc F c= F ';' G by FUNCT_4:33;
hence f = LastLoc (F ';' G) by A6, A8, A9, GRFUNC_1:8; :: thesis: verum

end;

suppose A10: f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) ; :: thesis: f = LastLoc (F ';' G)

then consider m being Element of NAT such that
A11: f = il. S,(m + ((card F) -' 1)) and
A12: il. S,m in dom (IncAddr G,((card F) -' 1)) by A2;
A13: il. S,m in dom G by A12, Def15;
then A14: pi G,(il. S,m) = G . (il. S,m) by AMI_1:def 47;
IncAddr (pi G,(il. S,m)),((card F) -' 1) = (IncAddr G,((card F) -' 1)) . (il. S,m) by A13, Def15
.= (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . (il. S,(m + ((card F) -' 1))) by A12, Def16
.= halt S by A6, A10, A11, FUNCT_4:14 ;
then G . (il. S,m) = halt S by A14, Th35;
then il. S,m = LastLoc G by A13, AMISTD_1:def 23
.= il. S,((card G) -' 1) by AMISTD_1:55 ;
then m = (card G) -' 1 by AMISTD_1:25;
then m + ((card F) -' 1) = (((card F) + (card G)) -' 1) -' 1 by A5, NAT_1:14, NAT_D:38
.= (card (F ';' G)) -' 1 by Th52 ;
hence f = LastLoc (F ';' G) by A11, AMISTD_1:55; :: thesis: verum

end;

end;