let s be State of SCM+FSA ; :: thesis: for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
let I be parahalting good Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
let a be read-write Int-Location ; :: thesis: ( I does_not_destroy a & s . a > 0 implies ( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) ) )
set I1 = I ';' (SubFrom a,(intloc 0 ));
set ss = IExec (I ';' (SubFrom a,(intloc 0 ))),s;
set s0 = Initialize s;
set ss0 = Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s);
set P = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
set s21 = (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
set s31 = (Initialize (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 ));
A1: I is_halting_on Initialize s by SCMFSA7B:25;
A2: I ';' (SubFrom a,(intloc 0 )) is_halting_on Initialize s by SCMFSA7B:25;
reconsider J3 = Macro (SubFrom a,(intloc 0 )) as good Program of SCM+FSA by Th99, SCMFSA7B:14;
set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
assume A3: I does_not_destroy a ; :: thesis: ( not s . a > 0 or ( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) ) )
0 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by Th54;
then A4: 0 in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:105;
A5: I ';' (SubFrom a,(intloc 0 )) is_closed_on Initialize s by SCMFSA7B:24;
A6: I ';' (SubFrom a,(intloc 0 )) = I ';' J3 ;
then A7: (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1 by A2, A5, Th96;
assume A8: s . a > 0 ; :: thesis: ( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
then A9: (Initialize s) . a > 0 by SCMFSA6C:3;
A10: (Initialize s) . (intloc 0 ) = 1 by SCMFSA6C:3;
then A11: loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on Initialize s by A3, A9, Th117;
A12: 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 A13: Directed (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on Initialize s by A3, A10, A9, Th117;
consider s2 being State of SCM+FSA , k being Element of NAT such that
A14: s2 = (Initialize s) +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) and
k = (LifeSpan ((Initialize s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 and
A15: (Comput (ProgramPart s2),s2,k) . a = ((Initialize s) . a) - 1 and
A16: (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 and
A17: for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,(Initialize s)) . b and
A18: for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,(Initialize s)) . f and
A19: IC (Comput (ProgramPart s2),s2,k) = 0 and
A20: 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 A3, A10, A9, Th122;

A21: now

let f be FinSeq-Location ; :: thesis: (Comput (ProgramPart s2),s2,k) . f = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . f
thus (Comput (ProgramPart s2),s2,k) . f = (IExec I,(Initialize s)) . f by A18
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . f by SCMFSA_2:91
.= (IExec (I ';' (SubFrom a,(intloc 0 ))),(Initialize s)) . f by SCMFSA6C:8
.= (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . f by Th17 ; :: thesis: verum

end;

thus A22: (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . a by SCMFSA6C:7
.= ((IExec I,s) . a) - ((IExec I,s) . (intloc 0 )) by SCMFSA_2:91
.= ((IExec I,s) . a) - 1 by A1, Th92
.= ((Initialize s) . a) - 1 by A3, Th91
.= (s . a) - 1 by SCMFSA6C:3 ; :: thesis: DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))

now

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

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

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

hence (Comput (ProgramPart s2),s2,k) . b = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b by A16, A6, A2, A5, Th96; :: thesis: verum

end;

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

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

end;

suppose A23: ( b <> a & b <> intloc 0 ) ; :: thesis: (Comput (ProgramPart s2),s2,k) . b₁ = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b₁

then reconsider bb = b as read-write Int-Location by SF_MASTR:def 5;
thus (Comput (ProgramPart s2),s2,k) . b = (IExec I,(Initialize s)) . bb by A17, A23
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . b by A23, SCMFSA_2:91
.= (IExec (I ';' (SubFrom a,(intloc 0 ))),(Initialize s)) . b by SCMFSA6C:7
.= (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b by Th17 ; :: thesis: verum

end;

end;

end;

then A24: DataPart (Comput (ProgramPart s2),s2,k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s) by A21, SCMFSA6A:38;
A25: DataPart (IExec (Times a,I),(Initialize s)) = DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(Initialize s)) by A3, A10, A9, A12, Th69, Th117;

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

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

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 A27: 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;
A28: (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;
then A29: (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124;
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: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 A31: (card (I ';' (SubFrom a,(intloc 0 )))) + 3 in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA6A:15;
(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, A31, A27, FUNCT_4:14
.= (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) by A31, SCMFSA6B:7 ;
then A32: (Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) = goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 5) by A28, A29, FUNCT_4:111;
then InsCode ((Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = 6 by SCMFSA_2:47;
then A33: InsCode ((Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) in {0 ,6,7,8} by ENUMSET1:def 2;
Y: (ProgramPart (Comput (ProgramPart s2),s2,k)) /. (IC (Comput (ProgramPart s2),s2,k)) = (Comput (ProgramPart s2),s2,k) . (IC (Comput (ProgramPart s2),s2,k)) by AMI_1:150;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,k) by AMI_1:144;
A34: Comput (ProgramPart s2),s2,(k + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,k) by AMI_1:14
.= Exec ((Comput (ProgramPart s2),s2,k) . 0 ),(Comput (ProgramPart s2),s2,k) by A19, Y, T ;
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 A35: 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;
A36: (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, A4, A35, FUNCT_4:14
.= (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) . 0 by A4, SCMFSA6B:7 ;
A37: (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 = a =0_goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) by Th55;
then (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124;
then A38: (Comput (ProgramPart s2),s2,k) . 0 = a =0_goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) by A36, A37, FUNCT_4:111;
A39: (Comput (ProgramPart s2),s2,k) . a = 0 by A15, A22, A26, SCMFSA6C:3;
then A40: IC (Comput (ProgramPart s2),s2,(k + 1)) = (card (I ';' (SubFrom a,(intloc 0 )))) + 3 by A34, A38, SCMFSA_2:96;

A41: now

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

end;

Y: (ProgramPart (Comput (ProgramPart s2),s2,(k + 1))) /. (IC (Comput (ProgramPart s2),s2,(k + 1))) = (Comput (ProgramPart s2),s2,(k + 1)) . (IC (Comput (ProgramPart s2),s2,(k + 1))) by AMI_1:150;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(k + 1)) by AMI_1:144;
A43: Comput (ProgramPart s2),s2,(k + (1 + 1)) = Comput (ProgramPart s2),s2,((k + 1) + 1)
.= Following (ProgramPart s2),(Comput (ProgramPart s2),s2,(k + 1)) by AMI_1:14
.= Exec ((Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)),(Comput (ProgramPart s2),s2,(k + 1)) by A39, A34, A38, Y, T, SCMFSA_2:96 ;
then IC (Comput (ProgramPart s2),s2,(k + 2)) = (card (I ';' (SubFrom a,(intloc 0 )))) + 5 by A32, SCMFSA_2:95
.= card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) by A30, AMI_1:105 ;
then A44: k + 2 = pseudo-LifeSpan (Initialize s),(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A14, A11, A41, SCMFSA8A:def 5;
InsCode ((Comput (ProgramPart s2),s2,k) . 0 ) = 7 by A38, SCMFSA_2:48;
then InsCode ((Comput (ProgramPart s2),s2,k) . 0 ) in {0 ,6,7,8} by ENUMSET1:def 2;
then DataPart (Comput (ProgramPart s2),s2,k) = DataPart (Comput (ProgramPart s2),s2,(k + 1)) by A34, Th32;
then A45: DataPart (Comput (ProgramPart s2),s2,k) = DataPart (Comput (ProgramPart s2),s2,(k + 2)) by A43, A33, Th32;
thus DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(Initialize s)) by Th17
.= DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s) by A25, Th17
.= DataPart ((Result (s +* (Initialized ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart ((Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) +* (s | NAT )) by SCMFSA8A:13
.= DataPart (Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) by Th35
.= DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s) by A3, A10, A9, A14, A12, A24, A44, A45, Th59, Th117
.= DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) by A7, A26, Th123 ; :: thesis: verum

end;

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

s . a >= 0 + 1 by A8, INT_1:20;
then A47: (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a > 0 by A22, A46, XREAL_1:21;
A48: DataPart (Initialize s) = DataPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
A49: k < pseudo-LifeSpan (Initialize s),(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A3, A10, A9, A14, A20, Th2, Th117;
then A50: DataPart (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize 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, A12, A13, A24, Th58;

A51: now

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

let a be Int-Location ; :: thesis: (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . b₁ = ((Initialize (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 ))) . b₁

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

suppose A53: a = intloc 0 ; :: thesis: (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . b₁ = ((Initialize (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 ))) . b₁

thus (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize 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 A50, SCMFSA6A:38
.= 1 by A53, SCMFSA6B:35
.= (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a by A53, SCMFSA6C:3
.= ((Initialize (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 A52, SCMFSA6A:38 ; :: thesis: verum

end;

suppose a <> intloc 0 ; :: thesis: (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . b₁ = ((Initialize (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 ))) . b₁

then A54: a is read-write Int-Location by SF_MASTR:def 5;
thus (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize 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 A50, SCMFSA6A:38
.= (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a by A54, SCMFSA6C:3
.= ((Initialize (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 A52, SCMFSA6A:38 ; :: thesis: verum

end;

end;

end;

let f be FinSeq-Location ; :: thesis: (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . f = ((Initialize (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
thus (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize 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 A50, SCMFSA6A:38
.= (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . f by SCMFSA6C:3
.= ((Initialize (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 A52, SCMFSA6A:38 ; :: thesis: verum

end;

IC (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize 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, A12, A13, A49, Th58
.= IC (((Initialize (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 A19, AMI_1:111
.= IC ((Initialize (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 A55: Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k,(Initialize (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 A51, SCMFSA6A:28;
A56: ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
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 A57: Directed (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by A3, A10, A9, A48, Th52, Th117;
then A58: (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ) is_closed_on (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by Th58;
A59: (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ) is_halting_on (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by A57, Th58;
A60: (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1 by A6, A2, A5, Th96;
A61: ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= (Initialize (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;
DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(Initialize s)) = DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s) by Th17
.= DataPart ((Result (s +* (Initialized ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart ((Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) +* (s | NAT )) by SCMFSA8A:13
.= DataPart (Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) by Th35
.= DataPart (Result ((Initialize (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 A56, A61, A58, A59, A55, Th103, SCMFSA6A:39
.= DataPart ((Result ((Initialize (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 Th35
.= DataPart ((Result ((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 SCMFSA8A:13
.= 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 A3, A12, A60, A47, Th69, Th117 ;
hence DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) by A25, Th17; :: thesis: verum

end;

end;