let s be State of ; :: thesis: for I being good InitHalting Program of
for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 holds
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
let I be good InitHalting Program of ; :: thesis: for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 holds
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
let a be read-write Int-Location ; :: thesis: ( I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 implies loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
set P = if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )));
reconsider I1 = I ';' (SubFrom a,(intloc 0 )) as InitHalting Program of ;
set i = a =0_goto (insloc ((card I1) + 3));
defpred S₁[ Element of NAT ] means for s being State of st s . (intloc 0 ) = 1 & s . a = $1 & s . a > 0 holds
( (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (s +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (s . a) - 1 & (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (s +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) );
assume A1: I does_not_destroy a ; :: thesis: ( not s . (intloc 0 ) = 1 or not s . a > 0 or loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

A3: now

InsCode (a =0_goto (insloc ((card I1) + 3))) = 7 by SCMFSA_2:48;
then A4: ( insloc 0 in dom (Macro (a =0_goto (insloc ((card I1) + 3)))) & (Macro (a =0_goto (insloc ((card I1) + 3)))) . (insloc 0 ) <> halt SCM+FSA ) by SCMFSA6B:32, SCMFSA6B:33, SCMFSA_2:124;
if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) = ((((a =0_goto (insloc ((card I1) + 3))) ';' I1) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= (((a =0_goto (insloc ((card I1) + 3))) ';' (I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1))))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA ) by SCMFSA6A:71
.= ((a =0_goto (insloc ((card I1) + 3))) ';' ((I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2)))) ';' (Stop SCM+FSA ) by SCMFSA6A:71
.= (a =0_goto (insloc ((card I1) + 3))) ';' (((I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA )) by SCMFSA6A:71
.= (Macro (a =0_goto (insloc ((card I1) + 3)))) ';' (((I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA )) ;
hence (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) = (Macro (a =0_goto (insloc ((card I1) + 3)))) . (insloc 0 ) by A4, SCMFSA6A:54
.= a =0_goto (insloc ((card I1) + 3)) by SCMFSA6B:33 ;
:: thesis: ( (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) <> halt SCM+FSA & insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )
hence (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124; :: thesis: ( insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )
A5: card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) = ((card (Goto (insloc 2))) + (card I1)) + 4 by SCMFSA8B:14
.= ((card I1) + 1) + 4 by SCMFSA8A:29
.= ((card I1) + 3) + 2 ;
hence insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by SCMFSA6A:15; :: thesis: ( (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )
card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = card (dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) by CARD_1:104
.= card (dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:105
.= card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by CARD_1:104 ;
then card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = (card I1) + (3 + 2) by A5, AMI_1:105;
hence (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) by SCMFSA8C:116; :: thesis: ( (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )
hence (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124; :: thesis: insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))

hereby :: thesis: verum

((card I1) + 3) + 0 < card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by A5, XREAL_1:8;
hence insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by SCMFSA6A:15; :: thesis: verum

end;

end;

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let ss be State of ; :: thesis: ( ss . (intloc 0 ) = 1 & ss . a = k + 1 & ss . a > 0 implies ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
assume A7: ss . (intloc 0 ) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
set s2 = ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))));
set s1 = ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))));
assume A8: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
A9: Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Following (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) by AMI_1:14
.= Exec (CurInstr (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))),(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) ;
set s3 = Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1);
assume A10: ss . a > 0 ; :: thesis: ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
A11: ( I1 is_closed_onInit ss & I1 is_halting_onInit ss ) by Th35, Th36;
then A12: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss by A10, Th45;
if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, A11, Th45;
then A13: Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Exec (goto (insloc 0 )),(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) by A12, A9, Th71;
A14: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, A11, Th45;

A15: now

A16: I1 is_halting_onInit ss by Th36;
then A17: I1 is_halting_on Initialize ss by Th41;
I1 is_closed_onInit ss by Th35;
then IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss = (IExec I1,ss) +* (Start-At (insloc (((card (Goto (insloc 2))) + (card I1)) + 3))) by A10, A16, Th46;
then A18: (IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss) . a = (IExec I1,ss) . a by SCMFSA_3:11;
A19: card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) = ((card (Goto (insloc 2))) + (card I1)) + 4 by SCMFSA8B:14
.= ((card I1) + 1) + 4 by SCMFSA8A:29
.= ((card I1) + 3) + 2 ;
A20: card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = card (dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) by CARD_1:104
.= card (dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:105
.= card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by CARD_1:104 ;

hereby :: thesis: ( (Initialize ss) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )

thus insloc 0 in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A20, A19, SCMFSA6A:15; :: thesis: insloc ((card I1) + 3) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
((card I1) + 3) + (1 + 1) = (((card I1) + 3) + 1) + 1 ;
then ((card I1) + 3) + 1 < card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by A19, NAT_1:13;
then (card I1) + 3 < card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A20, NAT_1:13;
hence insloc ((card I1) + 3) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA6A:15; :: thesis: verum

end;

consider Is being State of such that
A21: Is = (Initialize ss) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ;
Initialize (Initialize ss) = Initialize ss by SCMFSA8C:15;
then A22: Is = (Initialize ss) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))) by A21, SCMFSA8A:13;
I1 is_closed_onInit ss by Th35;
then A23: I1 is_closed_on Initialize ss by Th40;
I1 is_halting_onInit ss by Th36;
then A24: I1 is_halting_on Initialize ss by Th41;
A25: (Initialize ss) . a > 0 by A10, SCMFSA6C:3;
then A26: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialize ss by A23, A24, SCMFSA8B:18;
thus A27: (Initialize ss) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA8A:8; :: thesis: ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )

A28: now

let b be Int-Location ; :: thesis: (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Computation Is,(LifeSpan Is)) . b
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) . b by A13, SCMFSA_2:95;
hence (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Computation Is,(LifeSpan Is)) . b by A12, A14, A27, A21, Th68, SCMFSA6A:30; :: thesis: verum

end;

then (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (Computation Is,(LifeSpan Is)) . a
.= (IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss) . a by A22, A26, SCMFSA8C:87 ;
hence (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (Computation ((Initialize ss) +* (I1 +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* (I1 +* (Start-At (insloc 0 )))))) . a by A17, A18, SCMFSA8C:87
.= (ss . a) - 1 by A1, Th64 ;
:: thesis: (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1
A29: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is good by SCMFSA8C:115;
A30: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialize ss by A25, A23, A24, SCMFSA8B:18;
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = (Computation Is,(LifeSpan Is)) . (intloc 0 ) by A28
.= 1 by A22, A26, A30, A29, SCMFSA8C:96 ;
hence (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 ; :: thesis: verum

end;

hence ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 ) ; :: thesis: ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A31: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = insloc 0 by A13, SCMFSA_2:95;

hereby :: thesis: verum

per cases ( k = 0 or k > 0 ) ;

suppose A32: k = 0 ; :: thesis: ex m being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )

take m = (((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1) + 1; :: thesis: ( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A33: ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) by A7, SCMFSA8C:18;
A34: CurInstr (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) . (insloc 0 ) by A31, AMI_1:54
.= (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc 0 ) by A15, A33, SCMFSA8C:26
.= a =0_goto (insloc ((card I1) + 3)) by A3, FUNCT_4:111 ;
A35: Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1) = Following (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) by AMI_1:14
.= Exec (a =0_goto (insloc ((card I1) + 3))),(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) by A34 ;
then IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) = insloc ((card I1) + 3) by A8, A15, A32, SCMFSA_2:96;
then A36: CurInstr (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) = (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) . (insloc ((card I1) + 3)) by AMI_1:54
.= (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card I1) + 3)) by A15, A33, SCMFSA8C:26
.= goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) by A3, FUNCT_4:111 ;
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m = Following (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) by AMI_1:14
.= Exec (goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))),(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) by A36 ;
hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) by SCMFSA_2:95; :: thesis: for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < m implies IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )
assume n < m ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
then n <= ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 by NAT_1:13;
then A37: ( n <= (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 or n = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 ) by NAT_1:8;

per cases ( n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) or n = (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 or n = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 ) by A37, NAT_1:8;

suppose A38: n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

A39: ( I1 is_closed_onInit ss & I1 is_halting_onInit ss ) by Th35, Th36;
then A40: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, Th45;
if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss by A10, A39, Th45;
then Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n, Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n equal_outside NAT by A38, A40, Th68;
then A41: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n) by SCMFSA8A:6;
IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by A40, Def4;
hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A41, FUNCT_4:105; :: thesis: verum

end;

suppose n = (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A13, A15, SCMFSA_2:95; :: thesis: verum

end;

suppose n = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A8, A15, A32, A35, SCMFSA_2:96; :: thesis: verum

end;

end;

end;

end;

suppose A42: k > 0 ; :: thesis: ex m being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )

consider Is3 being State of such that
A43: Is3 = Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) ;
ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) c= Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by Th67, AMI_1:99;
then A44: loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) c= Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by AMI_1:105;
( Is3 . (intloc 0 ) = 1 & Is3 . a = k ) by A8, A15, A43, SCMFSA6C:3;
then consider m0 being Element of NAT such that
A45: IC (Computation (Is3 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m0) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) and
A46: for n being Element of NAT st n < m0 holds
IC (Computation (Is3 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A6, A42;
take m = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + m0; :: thesis: ( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A47: (Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) by SCMFSA8A:8
.= (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= ((Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= ((Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by Th19
.= (((Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:15
.= (Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA6C:def 3
.= (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A31, A15, SCMFSA8C:14
.= Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by A44, FUNCT_4:79 ;
hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) by A43, A45, AMI_1:51; :: thesis: for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < m implies IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )
assume A48: n < m ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
A49: ( I1 is_closed_onInit ss & I1 is_halting_onInit ss ) by Th35, Th36;
then A50: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, Th45;
A51: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss by A10, A49, Th45;

per cases ( n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) or (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 <= n ) by NAT_1:13;

suppose n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

then Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n, Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n equal_outside NAT by A50, A51, Th68;
then A52: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n) by SCMFSA8A:6;
IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by A50, Def4;
hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A52, FUNCT_4:105; :: thesis: verum

end;

suppose A53: (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 <= n ; :: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

consider mm being Element of NAT such that
A54: mm = n -' ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) ;
n - ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) >= 0 by A53, XREAL_1:50;
then A55: mm = n - ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by A54, XREAL_0:def 2;
mm + ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = n by A53, A54, XREAL_1:237;
then A56: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Computation (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)),mm) by AMI_1:51;
m0 = m - ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) ;
then mm < m0 by A48, A55, XREAL_1:11;
hence IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A43, A46, A47, A56; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

assume A57: s . (intloc 0 ) = 1 ; :: thesis: ( not s . a > 0 or loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
assume A58: s . a > 0 ; :: thesis: loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
then reconsider sa = s . a as Element of NAT by INT_1:16;
A59: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A59, A2);
then S₁[sa] ;
then A60: ex k being Element of NAT st
( IC (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) by A57, A58;
s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) by A57, SCMFSA8C:18;
hence loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s by A60, SCMFSA8A:def 3; :: thesis: verum