let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) )
let s be State of SCM+FSA; :: thesis: for I being good parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) )
let I be good parahalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) )
let a be read-write Int-Location; :: thesis: ( not I destroys a & s . a > 0 implies ( (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) ) )
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 Th70, SCMFSA7B:8;
set D = Data-Locations ;
assume A4: not I destroys a ; :: thesis: ( not s . a > 0 or ( (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) ) )
0 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by Th25;
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, Th67;
assume A9: s . a > 0 ; :: thesis: ( (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) )
then A10: (Initialized s) . a > 0 by SCMFSA_M:37;
A11: (Initialized s) . (intloc 0) = 1 by SCMFSA_M:9;
then A12: loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s,P by A4, A10, Th84;
A13: 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 A14: Directed (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialized s,P by A4, A11, A10, Th84;
consider s2 being State of SCM+FSA, P2 being Instruction-Sequence of SCM+FSA, k being Element of NAT such that
A15: s2 = Initialize (Initialized s) and
A16: 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
A17: (Comput (P2,s2,k)) . a = ((Initialized s) . a) - 1 and
A18: (Comput (P2,s2,k)) . (intloc 0) = 1 and
A19: for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,(Initialized s))) . b and
A20: for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,(Initialized s))) . f and
A21: IC (Comput (P2,s2,k)) = 0 and
A22: 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, Th89;

A23: now :: thesis: for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . f

let f be FinSeq-Location ; :: thesis: (Comput (P2,s2,k)) . f = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . f
thus (Comput (P2,s2,k)) . f = (IExec (I,P,(Initialized s))) . f by A20
.= (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: verum

end;

thus A24: (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, Th63
.= ((Initialized s) . a) - 1 by A4, Th62
.= (s . a) - 1 by SCMFSA_M:37 ; :: thesis: DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))

now :: thesis: for b being Int-Location holds (Comput (P2,s2,k)) . b = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b

let b be Int-Location; :: thesis: (Comput (P2,s2,k)) . b₁ = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b₁

per cases ( b = intloc 0 or b = a or ( b <> a & b <> intloc 0 ) ) ;

suppose b = intloc 0 ; :: thesis: (Comput (P2,s2,k)) . b₁ = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b₁

hence (Comput (P2,s2,k)) . b = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b by A18, A7, A3, A6, Th67; :: thesis: verum

end;

suppose b = a ; :: thesis: (Comput (P2,s2,k)) . b₁ = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b₁

hence (Comput (P2,s2,k)) . b = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b by A17, A24, SCMFSA_M:37; :: thesis: verum

end;

suppose A25: ( b <> a & b <> intloc 0 ) ; :: thesis: (Comput (P2,s2,k)) . b₁ = (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . b₁

then reconsider bb = b as read-write Int-Location by SCMFSA_M:def 2;
thus (Comput (P2,s2,k)) . b = (IExec (I,P,(Initialized s))) . bb by A19, A25
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,(Initialized s))))) . b by A25, 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: verum

end;

end;

end;

then A26: DataPart (Comput (P2,s2,k)) = DataPart (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) by A23, SCMFSA_M:2;
A27: 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, A13, Th40, Th84;

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

suppose A28: (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = 0 ; :: thesis: DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))

A29: (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 Th36;
A30: (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 A31: (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 A31, A16, FUNCT_4:13
.= (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) ;
then A32: P2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 5) by A29, FUNCT_4:105;
then InsCode (P2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3)) = 6 by SCMFSA_2:23;
then A33: InsCode (P2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3)) in {0,6,7,8} by ENUMSET1:def 2;
A34: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3
.= Exec ((P2 . 0),(Comput (P2,s2,k))) by A21, PBOOLE:143 ;
A35: P2 . 0 = (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . 0 by A5, A16, FUNCT_4:13
.= (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . 0 ;
A36: (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 = a =0_goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) by Th26;
A37: P2 . 0 = a =0_goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) by A35, A36, FUNCT_4:105;
A38: (Comput (P2,s2,k)) . a = 0 by A17, A24, A28, SCMFSA_M:37;
then A39: IC (Comput (P2,s2,(k + 1))) = (card (I ";" (SubFrom (a,(intloc 0))))) + 3 by A34, A37, SCMFSA_2:70;

A40: now :: thesis: for n being Element of NAT st not IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) holds
k + (1 + 1) <= n

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

end;

A42: P2 /. (IC (Comput (P2,s2,(k + 1)))) = P2 . (IC (Comput (P2,s2,(k + 1)))) by PBOOLE:143;
A43: 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 A38, A34, A37, A42, SCMFSA_2:70 ;
then IC (Comput (P2,s2,(k + 2))) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A30, A32, SCMFSA_2:69;
then A44: k + 2 = pseudo-LifeSpan ((Initialized s),P,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by A15, A12, A40, A16, SCMFSA8A:def 4;
InsCode (P2 . 0) = 7 by A37, 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 A34, Th12;
then A45: DataPart (Comput (P2,s2,k)) = DataPart (Comput (P2,s2,(k + 2))) by A43, A33, Th12;
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 A27
.= 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, A15, A13, A26, A44, A45, Th30, Th84, A16
.= DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) by A8, A28, Th90 ; :: thesis: verum

end;

suppose A46: (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a <> 0 ; :: thesis: DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))

s . a >= 0 + 1 by A9, INT_1:7;
then A47: (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a > 0 by A24, A46, XREAL_1:19;
A48: DataPart (Initialized s) = DataPart (Initialize (Initialized s)) by MEMSTR_0:79;
A49: k < pseudo-LifeSpan ((Initialized s),P,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by A4, A11, A10, A15, A22, Th1, Th84, A16;
then A50: 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 A15, A13, A14, A26, Th29, A16;

A51: now :: thesis: ( ( for a being Int-Location holds (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . a = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . f = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . f ) )

A52: 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: for f being FinSeq-Location holds (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . f = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . f

let a be Int-Location; :: thesis: (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . b₁ = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . b₁

per cases ( a = intloc 0 or a <> intloc 0 ) ;

suppose A53: a = intloc 0 ; :: thesis: (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . b₁ = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . b₁

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 A50, SCMFSA_M:2
.= 1 by A53, SCMFSA6B:11
.= (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))) . a by A53, SCMFSA_M:9
.= (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . a by A52, SCMFSA_M:2 ; :: thesis: verum

end;

suppose a <> intloc 0 ; :: thesis: (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . b₁ = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . b₁

then A54: a is read-write Int-Location by SCMFSA_M:def 2;
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 A50, SCMFSA_M:2
.= (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))) . a by A54, SCMFSA_M:37
.= (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . a by A52, SCMFSA_M:2 ; :: thesis: verum

end;

end;

end;

let f be FinSeq-Location ; :: thesis: (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . f = (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . f
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 A50, SCMFSA_M:2
.= (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))) . f by SCMFSA_M:37
.= (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) . f by A52, SCMFSA_M:2 ; :: thesis: verum

end;

IC (Comput ((P +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) = 0 by A21, A15, A13, A14, A49, Th29, A16
.= IC (Initialize (Initialized (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s))))) by FUNCT_4:113 ;
then A55: 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 A51, 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 A56: 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, A48, Th23, Th84;
then A57: (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 Th29;
A58: (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 A56, Th29;
A59: (IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . (intloc 0) = 1 by A7, A3, A6, Th67;
A60: 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 A57, A58, A55, Th73, 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 A60
.= 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, A13, A59, A47, Th40, Th84 ;
hence DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)))) by A27; :: thesis: verum

end;

end;