let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let I be good parahalting Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
set I1 = I ';' (SubFrom (a,(intloc 0)));
set ss = IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s);
set PP = P;
set s0 = Initialized s;
set ss0 = Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s));
set PP0 = P;
set I2 = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
set s21 = Initialize (Initialized s);
set P21 = P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA));
set s31 = Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))));
set P31 = P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA));
A1: (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA) c= P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) by FUNCT_4:25;
A2: I is_halting_on Initialized s,P by SCMFSA7B:19;
A3: I ';' (SubFrom (a,(intloc 0))) is_halting_on Initialized s,P by SCMFSA7B:19;
reconsider J3 = Macro (SubFrom (a,(intloc 0))) as good Program of SCM+FSA by Th99, SCMFSA7B:8;
set D = Data-Locations ;
set A = NAT ;
assume A4: not I destroys a ; :: thesis:
0 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by Th54;
then A5: 0 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:99;
A6: I ';' (SubFrom (a,(intloc 0))) is_closed_on Initialized s,P by SCMFSA7B:18;
A7: I ';' (SubFrom (a,(intloc 0))) = I ';' J3 ;
then A8: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . (intloc 0) = 1 by A3, A6, Th96;
assume A9: s . a > 0 ; :: thesis:
then A10: (Initialized s) . a > 0 by SCMFSA6C:3;
A11: (Initialized s) . (intloc 0) = 1 by SCMFSA6A:38;
then A12: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s,P by A4, A10, Th117;
A14: Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by SCMFSA6A:22;
then A15: Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialized s,P by A4, A11, A10, Th117;
consider s2 being State of SCM+FSA, P2 being Instruction-Sequence of SCM+FSA, k being Element of NAT such that
A16: s2 = Initialize (Initialized s) and
A17: P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) and
k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)))) + 1 and
A18: (Comput (P2,s2,k)) . a = ((Initialized s) . a) - 1 and
A19: (Comput (P2,s2,k)) . (intloc 0) = 1 and
A20: for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,(Initialized s))) . b and
A21: for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,(Initialized s))) . f and
A22: IC (Comput (P2,s2,k)) = 0 and
A23: for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A4, A11, A10, Th122;

A24: now

let f be FinSeq-Location ; :: thesis:
thus (Comput (P2,s2,k)) . f = (IExec (I,P,(Initialized s))) . f by A21
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,(Initialized s))))) . f by SCMFSA_2:65
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,(Initialized s))) . f by SCMFSA6C:7
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . f ; :: thesis:

end;

thus A25: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,s)))) . a by SCMFSA6C:6
.= ((IExec (I,P,s)) . a) - ((IExec (I,P,s)) . (intloc 0)) by SCMFSA_2:65
.= ((IExec (I,P,s)) . a) - 1 by A2, Th92
.= ((Initialized s) . a) - 1 by A4, Th91
.= (s . a) - 1 by SCMFSA6C:3 ; :: thesis:

let b be Int-Location ; :: thesis:

suppose b = intloc 0 ; :: thesis:

hence (Comput (P2,s2,k)) . b = (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . b by A19, A7, A3, A6, Th96; :: thesis:

end;

suppose b = a ; :: thesis:

hence (Comput (P2,s2,k)) . b = (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . b by A18, A25, SCMFSA6C:3; :: thesis:

end;

suppose A26: ( b <> a & b <> intloc 0 ) ; :: thesis:

then reconsider bb = b as read-write Int-Location by SF_MASTR:def 5;
thus (Comput (P2,s2,k)) . b = (IExec (I,P,(Initialized s))) . bb by A20, A26
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,(Initialized s))))) . b by A26, SCMFSA_2:65
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,(Initialized s))) . b by SCMFSA6C:6
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . b ; :: thesis:

end;

end;

end;

then A27: DataPart (Comput (P2,s2,k)) = DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) by A24, SCMFSA6A:7;
A28: DataPart (IExec ((Times (a,I)),P,(Initialized s))) = DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),P,(Initialized s))) by A4, A11, A10, A14, Th69, Th117;

per cases ) . a = 0 or (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a <> 0 ) ;

suppose A29: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a = 0 ; :: thesis:

A30: (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5) by Th65;
A31: (card (I ';' (SubFrom (a,(intloc 0))))) + (3 + 2) = ((card (I ';' (SubFrom (a,(intloc 0))))) + 1) + 4
.= ((card (Goto 2)) + (card (I ';' (SubFrom (a,(intloc 0)))))) + 4 by SCMFSA8A:15
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by SCMFSA8B:11
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
.= card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by FUNCT_4:99
.= card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ;
then ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) + 0 < card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by XREAL_1:6;
then A32: (card (I ';' (SubFrom (a,(intloc 0))))) + 3 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by AFINSQ_1:66;
P2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by A32, A17, FUNCT_4:13
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) ;
then A33: P2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5) by A30, FUNCT_4:105;
then InsCode (P2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) = 6 by SCMFSA_2:23;
then A34: InsCode (P2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) in {0,6,7,8} by ENUMSET1:def 2;
A36: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3
.= Exec ((P2 . 0),(Comput (P2,s2,k))) by A22, PBOOLE:143 ;
A37: P2 . 0 = (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 by A5, A17, FUNCT_4:13
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 ;
A38: (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . 0 = a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by Th55;
A39: P2 . 0 = a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by A37, A38, FUNCT_4:105;
A40: (Comput (P2,s2,k)) . a = 0 by A18, A25, A29, SCMFSA6C:3;
then A41: IC (Comput (P2,s2,(k + 1))) = (card (I ';' (SubFrom (a,(intloc 0))))) + 3 by A36, A39, SCMFSA_2:70;

A42: now

let n be Element of NAT ; :: thesis:
assume A43: not IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ; :: thesis:
then k < n by A23;
then k + 1 <= n by INT_1:7;
then k + 1 < n by A41, A32, A43, XXREAL_0:1;
then (k + 1) + 1 <= n by INT_1:7;
hence k + (1 + 1) <= n ; :: thesis:

end;

A44: P2 /. (IC (Comput (P2,s2,(k + 1)))) = P2 . (IC (Comput (P2,s2,(k + 1)))) by PBOOLE:143;
A45: Comput (P2,s2,(k + (1 + 1))) = Comput (P2,s2,((k + 1) + 1))
.= Following (P2,(Comput (P2,s2,(k + 1)))) by EXTPRO_1:3
.= Exec ((P2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)),(Comput (P2,s2,(k + 1)))) by A40, A36, A39, A44, SCMFSA_2:70 ;
then IC (Comput (P2,s2,(k + 2))) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A31, A33, SCMFSA_2:69;
then A46: k + 2 = pseudo-LifeSpan ((Initialized s),P,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A16, A12, A42, A17, SCMFSA8A:def 4;
InsCode (P2 . 0) = 7 by A39, SCMFSA_2:24;
then InsCode (P2 . 0) in {0,6,7,8} by ENUMSET1:def 2;
then DataPart (Comput (P2,s2,k)) = DataPart (Comput (P2,s2,(k + 1))) by A36, Th32;
then A47: DataPart (Comput (P2,s2,k)) = DataPart (Comput (P2,s2,(k + 2))) by A45, A34, Th32;
thus DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(Initialized s)))
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),P,s)) by A28
.= DataPart (Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)))) by MEMSTR_0:44
.= DataPart (Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s))))
.= DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) by A4, A11, A10, A16, A14, A27, A46, A47, Th59, Th117, A17
.= DataPart (IExec ((Times (a,I)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) by A8, A29, Th123 ; :: thesis:

end;

suppose A49: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a <> 0 ; :: thesis:

s . a >= 0 + 1 by A9, INT_1:7;
then A50: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a > 0 by A25, A49, XREAL_1:19;
A51: DataPart (Initialized s) = DataPart (Initialize (Initialized s)) by MEMSTR_0:79;
A52: k < pseudo-LifeSpan ((Initialized s),P,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A4, A11, A10, A16, A23, Th2, Th117, A17;
then A53: DataPart (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)),k)) = DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) by A16, A14, A15, A27, Th58, A17;

A54: now

A55: DataPart (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))) = DataPart (Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))))) by MEMSTR_0:79;

hereby :: thesis:

let a be Int-Location ; :: thesis:

suppose A56: a = intloc 0 ; :: thesis:

thus (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . a = (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a by A53, SCMFSA6A:7
.= 1 by A56, SCMFSA6B:11
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))) . a by A56, SCMFSA6A:38
.= (Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))))) . a by A55, SCMFSA6A:7 ; :: thesis:

end;

suppose a <> intloc 0 ; :: thesis:

then A57: a is read-write Int-Location by SF_MASTR:def 5;
thus (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . a = (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a by A53, SCMFSA6A:7
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))) . a by A57, SCMFSA6C:3
.= (Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))))) . a by A55, SCMFSA6A:7 ; :: thesis:

end;

end;

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . f = (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . f by A53, SCMFSA6A:7
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))) . f by SCMFSA6C:3
.= (Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))))) . f by A55, SCMFSA6A:7 ; :: thesis:

end;

IC (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)),k)) = 0 by A22, A16, A14, A15, A52, Th58, A17
.= IC (Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))))) by FUNCT_4:113 ;
then A58: Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)),k) = Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) by A54, SCMFSA_2:61;
Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by SCMFSA6A:22;
then A60: Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialize (Initialized s),P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) by A4, A11, A10, A51, Th52, Th117;
then A61: (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA) is_closed_on Initialize (Initialized s),P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) by Th58;
A62: (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA) is_halting_on Initialize (Initialized s),P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) by A60, Th58;
A63: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . (intloc 0) = 1 by A7, A3, A6, Th96;
XX: Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s))) = Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))))) by A61, A62, A58, Th103, A1;
DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),P,(Initialized s))) = DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),P,s))
.= DataPart (Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s)))) by MEMSTR_0:44
.= DataPart (Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized s))))
.= DataPart (Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s))))))) by XX
.= DataPart (Result ((P +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),(Initialize (Initialized (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))))))
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) by MEMSTR_0:44
.= DataPart (IExec ((Times (a,I)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) by A4, A14, A63, A50, Th69, Th117 ;
hence DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) by A28; :: thesis:

end;

end;