let s be State of SCM+FSA; :: thesis:
let I be good InitHalting Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
assume A1: not I destroys a ; :: thesis:
reconsider J3 = Macro (SubFrom (a,(intloc 0))) as good Program of SCM+FSA ;
set I1 = I ';' (SubFrom (a,(intloc 0)));
set ss = IExec ((I ';' (SubFrom (a,(intloc 0)))),s);
I ';' (SubFrom (a,(intloc 0))) is_closed_onInit s by Th35;
then A2: I ';' (SubFrom (a,(intloc 0))) is_closed_on Initialized s by Th40;
I ';' (SubFrom (a,(intloc 0))) is_halting_onInit s by Th36;
then A3: ( I ';' (SubFrom (a,(intloc 0))) = I ';' J3 & I ';' (SubFrom (a,(intloc 0))) is_halting_on Initialized s ) by Th41;
then A4: (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . (intloc 0) = 1 by A2, SCMFSA8C:96;
set P = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
set s0 = Initialized s;
assume A5: s . a > 0 ; :: thesis:
then A6: (Initialized s) . a > 0 by SCMFSA6C:3;
then consider s2 being State of SCM+FSA, k being Element of NAT such that
A7: s2 = (Initialized s) +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) and
k = (LifeSpan ((ProgramPart ((Initialized s) +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((Initialized s) +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1 and
A8: (Comput ((ProgramPart s2),s2,k)) . a = ((Initialized s) . a) - 1 and
A9: (Comput ((ProgramPart s2),s2,k)) . (intloc 0) = 1 and
A10: for b being read-write Int-Location st b <> a holds
(Comput ((ProgramPart s2),s2,k)) . b = (IExec (I,(Initialized s))) . b and
A11: for f being FinSeq-Location holds (Comput ((ProgramPart s2),s2,k)) . f = (IExec (I,(Initialized s))) . f and
A12: IC (Comput ((ProgramPart s2),s2,k)) = 0 and
A13: for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart s2),s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A1, Th77;
A14: s2 = (Initialized (Initialized s)) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) by A7, SCMFSA8A:13
.= (Initialized s) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) by SCMFSA8C:15 ;

A15: now

let f be FinSeq-Location ; :: thesis:
thus (Comput ((ProgramPart s2),s2,k)) . f = (IExec (I,(Initialized s))) . f by A11
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,(Initialized s))))) . f by SCMFSA_2:91
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),(Initialized s))) . f by Th34
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . f by SCMFSA8C:17 ; :: thesis:

end;

thus A16: (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,s)))) . a by Th33
.= ((IExec (I,s)) . a) - ((IExec (I,s)) . (intloc 0)) by SCMFSA_2:91
.= ((IExec (I,s)) . a) - 1 by Th17
.= ((Initialized s) . a) - 1 by A1, Th63
.= (s . a) - 1 by SCMFSA6C:3 ; :: thesis:

now

let b be Int-Location ; :: thesis:

per cases ;

suppose b = intloc 0 ; :: thesis:

hence (Comput ((ProgramPart s2),s2,k)) . b = (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . b by A9, A3, A2, SCMFSA8C:96; :: thesis:

end;

suppose b = a ; :: thesis:

hence (Comput ((ProgramPart s2),s2,k)) . b = (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . b by A8, A16, SCMFSA6C:3; :: thesis:

end;

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

then reconsider bb = b as read-write Int-Location by SF_MASTR:def 5;
thus (Comput ((ProgramPart s2),s2,k)) . b = (IExec (I,(Initialized s))) . bb by A10, A17
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,(Initialized s))))) . b by A17, SCMFSA_2:91
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),(Initialized s))) . b by Th33
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . b by SCMFSA8C:17 ; :: thesis:

end;

end;

end;

then A18: DataPart (Comput ((ProgramPart s2),s2,k)) = DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) by A15, SCMFSA6A:38;
set s21 = (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)));
set ss0 = Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s));
set s31 = (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)));
0 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by SCMFSA8C:54;
then A19: 0 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:105;
A20: (Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
then A21: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s by A1, A6, Th73;
A22: 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:63;
then A23: Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialized s by A1, A20, A6, Th73;
A24: DataPart (IExec ((Times (a,I)),(Initialized s))) = DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),(Initialized s))) by A1, A20, A6, A22, Th73, SCMFSA8C:69;

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

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

loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) c= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A26: dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) c= dom ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
A27: (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 SCMFSA8C:65;
A29: (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:29
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by SCMFSA8B:14
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by CARD_1:104
.= card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by FUNCT_4:105
.= card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by CARD_1:104 ;
then ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) + 0 < card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by XREAL_1:8;
then A30: (card (I ';' (SubFrom (a,(intloc 0))))) + 3 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by AFINSQ_1:70;
(Comput ((ProgramPart s2),s2,(k + 1))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = s2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by AMI_1:54
.= ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by A14, A30, A26, FUNCT_4:14
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by A30, SCMFSA6B:7 ;
then A31: (Comput ((ProgramPart s2),s2,(k + 1))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5) by A27, FUNCT_4:111;
loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) c= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A32: dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) c= dom ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
A33: (Comput ((ProgramPart s2),s2,k)) . 0 = s2 . 0 by AMI_1:54
.= ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) . 0 by A14, A19, A32, FUNCT_4:14
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 by A19, SCMFSA6B:7 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,k)) by AMI_1:123;
Y: (ProgramPart s2) /. (IC (Comput ((ProgramPart s2),s2,k))) = (Comput ((ProgramPart s2),s2,k)) . (IC (Comput ((ProgramPart s2),s2,k))) by T, COMPOS_1:38;
A34: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec (((Comput ((ProgramPart s2),s2,k)) . 0),(Comput ((ProgramPart s2),s2,k))) by A12, Y ;
A35: (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . 0 = a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by SCMFSA8C:55;
A36: (Comput ((ProgramPart s2),s2,k)) . 0 = a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by A33, A35, FUNCT_4:111;
then InsCode ((Comput ((ProgramPart s2),s2,k)) . 0) = 7 by SCMFSA_2:48;
then InsCode ((Comput ((ProgramPart s2),s2,k)) . 0) in {0,6,7,8} by ENUMSET1:def 2;
then A37: DataPart (Comput ((ProgramPart s2),s2,k)) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) by A34, SCMFSA8C:32;
A38: (Comput ((ProgramPart s2),s2,k)) . a = 0 by A8, A16, A25, SCMFSA6C:3;
then A39: IC (Comput ((ProgramPart s2),s2,(k + 1))) = (card (I ';' (SubFrom (a,(intloc 0))))) + 3 by A34, A36, SCMFSA_2:96;

A40: now

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

end;

T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,(k + 1))) by AMI_1:123;
Y: (ProgramPart s2) /. (IC (Comput ((ProgramPart s2),s2,(k + 1)))) = (Comput ((ProgramPart s2),s2,(k + 1))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by T, COMPOS_1:38;
A42: Comput ((ProgramPart s2),s2,(k + (1 + 1))) = Comput ((ProgramPart s2),s2,((k + 1) + 1))
.= Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(k + 1)))) by EXTPRO_1:4
.= Exec (((Comput ((ProgramPart s2),s2,(k + 1))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)),(Comput ((ProgramPart s2),s2,(k + 1)))) by A38, A34, A36, Y, SCMFSA_2:96 ;
then IC (Comput ((ProgramPart s2),s2,(k + 2))) = (card (I ';' (SubFrom (a,(intloc 0))))) + 5 by A31, SCMFSA_2:95
.= card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A29, RELAT_1:209 ;
then A43: k + 2 = pseudo-LifeSpan ((Initialized s),(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A14, A21, A40, SCMFSA8A:def 5;
InsCode ((Comput ((ProgramPart s2),s2,(k + 1))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) = 6 by A31, SCMFSA_2:47;
then InsCode ((Comput ((ProgramPart s2),s2,(k + 1))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) in {0,6,7,8} by ENUMSET1:def 2;
then A44: DataPart (Comput ((ProgramPart s2),s2,k)) = DataPart (Comput ((ProgramPart s2),s2,(k + 2))) by A37, A42, SCMFSA8C:32;
X: (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) = s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) by SCMFSA8A:13;
thus DataPart (IExec ((Times (a,I)),s)) = DataPart (IExec ((Times (a,I)),(Initialized s))) by SCMFSA8C:17
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),s)) by A24, SCMFSA8C:17
.= DataPart ((Result ((ProgramPart (s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))))),(s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart ((Result ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) +* (s | NAT)) by X
.= DataPart (Result ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) by SCMFSA8C:35
.= DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) by A1, A20, A6, A14, A22, A18, A43, A44, Th73, SCMFSA8C:59
.= DataPart (IExec ((Times (a,I)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) by A4, A25, Th78 ; :: thesis:

end;

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

s . a >= 0 + 1 by A5, INT_1:20;
then A46: (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . a > 0 by A16, A45, XREAL_1:21;
A47: ( ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)) c= (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) & ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)) c= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) ) by FUNCT_4:26;
A48: k < pseudo-LifeSpan ((Initialized s),(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A1, A20, A6, A13, A14, Th73, SCMFSA8C:2;
then A49: DataPart (Comput ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) = DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) by A14, A22, A23, A18, SCMFSA8C:58;

A50: now

A51: DataPart (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) = DataPart ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;

hereby :: thesis:

let a be Int-Location ; :: thesis:

per cases ;

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

thus (Comput ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) . a = (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . a by A49, SCMFSA6A:38
.= 1 by A52, Th17
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) . a by A52, SCMFSA6C:3
.= ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . a by A51, SCMFSA6A:38 ; :: thesis:

end;

suppose a <> intloc 0 ; :: thesis:

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

end;

end;

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) . f = (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . f by A49, SCMFSA6A:38
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) . f by SCMFSA6C:3
.= ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . f by A51, SCMFSA6A:38 ; :: thesis:

end;

IC (Comput ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart s2),s2,k)) by A14, A22, A23, A48, SCMFSA8C:58
.= IC (((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) +* (Start-At (0,SCM+FSA))) by A12, FUNCT_4:121
.= IC ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15 ;
then A54: Comput ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k),(Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) equal_outside NAT by A50, SCMFSA10:91;
A55: (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . (intloc 0) = 1 by A3, A2, SCMFSA8C:96;
( Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) & DataPart (Initialized s) = DataPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) ) by SCMFSA6A:63, SCMFSA8A:11;
then Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by A1, A20, A6, Th73, SCMFSA8C:52;
then A56: ( (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA) is_closed_on (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) & (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA) is_halting_on (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) ) by SCMFSA8C:58;
X: (Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) = s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) by SCMFSA8A:13;
Y: (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) = (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) by SCMFSA8A:13;
DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),(Initialized s))) = DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),s)) by SCMFSA8C:17
.= DataPart ((Result ((ProgramPart (s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))))),(s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart ((Result ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) +* (s | NAT)) by X
.= DataPart (Result ((ProgramPart ((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) by SCMFSA8C:35
.= DataPart (Result ((ProgramPart ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) by A47, A56, A54, SCMFSA6A:39, SCMFSA8C:103
.= DataPart ((Result ((ProgramPart ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),s))) +* (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) +* ((IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) | NAT)) by SCMFSA8C:35
.= DataPart ((Result ((ProgramPart ((IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))))),((IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) +* ((IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) | NAT)) by Y
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) by SCMFSA6B:def 1
.= DataPart (IExec ((Times (a,I)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) by A1, A22, A55, A46, Th73, SCMFSA8C:69 ;
hence DataPart (IExec ((Times (a,I)),s)) = DataPart (IExec ((Times (a,I)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) by A24, SCMFSA8C:17; :: thesis:

end;

end;