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

A4: ( 0 in dom (Macro (a =0_goto ((card I1) + 3))) & (Macro (a =0_goto ((card I1) + 3))) . 0 <> halt SCM+FSA ) by COMPOS_1:148, SCMFSA6B:32;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) = ((((a =0_goto ((card I1) + 3)) ';' I1) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA) by SCMFSA8B:def 1
.= (((a =0_goto ((card I1) + 3)) ';' (I1 ';' (Goto ((card (Goto 2)) + 1)))) ';' (Goto 2)) ';' (Stop SCM+FSA) by SCMFSA6A:71
.= ((a =0_goto ((card I1) + 3)) ';' ((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2))) ';' (Stop SCM+FSA) by SCMFSA6A:71
.= (a =0_goto ((card I1) + 3)) ';' (((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA)) by SCMFSA6A:71
.= (Macro (a =0_goto ((card I1) + 3))) ';' (((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA)) ;
hence (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . 0 = (Macro (a =0_goto ((card I1) + 3))) . 0 by A4, SCMFSA6A:54
.= a =0_goto ((card I1) + 3) by COMPOS_1:148 ;
:: thesis: ( (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . 0 <> halt SCM+FSA & 0 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) & (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) & (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) )
hence (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . 0 <> halt SCM+FSA ; :: thesis: ( 0 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) & (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) & (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) )
A5: card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:14
.= ((card I1) + 1) + 4 by SCMFSA8A:29
.= ((card I1) + 3) + 2 ;
hence 0 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by AFINSQ_1:70; :: thesis: ( (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) & (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) )
card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by CARD_1:104
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:105
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by CARD_1:104 ;
then card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) = (card I1) + (3 + 2) by A5, RELAT_1:209;
hence (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) by SCMFSA8C:116; :: thesis: ( (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) )
hence (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA ; :: thesis: (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))

hereby :: thesis: verum

((card I1) + 3) + 0 < card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A5, XREAL_1:8;
hence (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by AFINSQ_1:70; :: 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 SCM+FSA; :: thesis: ( ss . (intloc 0) = 1 & ss . a = k + 1 & ss . a > 0 implies ( (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),k)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
assume A7: ss . (intloc 0) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),k)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
set s2 = ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))));
set s1 = ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))));
assume A8: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),k)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
A9: Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1)) = Following ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))))))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))))))),(Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))))))) ;
set s3 = Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1));
assume A10: ss . a > 0 ; :: thesis: ( (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),k)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 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 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit ss by A10, Th45;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss by A10, A11, Th45;
then A13: Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1)) = Exec ((goto 0),(Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))))))) by A12, A9, Th71;
A14: if=0 (a,(Goto 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 Initialized ss by Th41;
I1 is_closed_onInit ss by Th35;
then IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),ss) = (IExec (I1,ss)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A10, A16, Th46;
then A18: (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),ss)) . a = (IExec (I1,ss)) . a by SCMFSA_3:11;
A19: card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) = ((card (Goto 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 2),(I ';' (SubFrom (a,(intloc 0))))))) = card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by CARD_1:104
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:105
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by CARD_1:104 ;

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

thus 0 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A20, A19, AFINSQ_1:70; :: thesis: (card I1) + 3 in dom (loop (if=0 (a,(Goto 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 2),(I ';' (SubFrom (a,(intloc 0)))))) by A19, NAT_1:13;
then (card I1) + 3 < card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A20, NAT_1:13;
hence (card I1) + 3 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by AFINSQ_1:70; :: thesis: verum

end;

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

A28: now

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

end;

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

end;

hence ( (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) . (intloc 0) = 1 ) ; :: thesis: ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),k)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A31: IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) = 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 (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),m)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

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

hereby :: thesis: verum

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

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

suppose A38: n <= LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) ; :: thesis: IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),b₁)) in dom (loop (if=0 (a,(Goto 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 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss by A10, Th45;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit ss by A10, A39, Th45;
then Comput ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),n), Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n) equal_outside NAT by A38, A40, Th68;
then A41: IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) = IC (Comput ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),n)) by SCMFSA8A:6;
IC (Comput ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A40, Def4;
hence IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A41, FUNCT_4:105; :: thesis: verum

end;

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

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

end;

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

hence IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 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 (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),m)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

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

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < m implies IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume A48: n < m ; :: thesis: IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),b₁)) in dom (loop (if=0 (a,(Goto 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 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss by A10, Th45;
A51: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit ss by A10, A49, Th45;

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

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

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

end;

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

consider mm being Element of NAT such that
A54: mm = n -' ((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1) ;
n - ((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1) >= 0 by A53, XREAL_1:50;
then A55: mm = n - ((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1) by A54, XREAL_0:def 2;
T: ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) = ProgramPart (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))) by AMI_1:123;
mm + ((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1) = n by A53, A54, XREAL_1:237;
then A56: IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) = IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1))),mm)) by EXTPRO_1:5;
m0 = m - ((LifeSpan ((ProgramPart (ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(ss +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1) ;
then mm < m0 by A48, A55, XREAL_1:11;
hence IC (Comput ((ProgramPart (ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(ss +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A43, A46, A47, A56, T; :: 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 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s )
assume A58: s . a > 0 ; :: thesis: loop (if=0 (a,(Goto 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 (Comput ((ProgramPart (s +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(s +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),k)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (s +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(s +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) by A57, A58;
s +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) = s +* (Initialize (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A57, SCMFSA8C:18;
hence loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s by A60, SCMFSA8A:def 3; :: thesis: verum