let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
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,p
let p be Instruction-Sequence 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,p
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,p
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,p )
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
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & s . a = $1 & s . a > 0 holds
( (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized s),((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1))) . a = (s . a) - 1 & (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized s),((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized s),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized s),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,p )
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:58, COMPOS_1:60;
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:29
.= ((a =0_goto ((card I1) + 3)) ';' ((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2))) ';' (Stop SCM+FSA) by SCMFSA6A:29
.= (a =0_goto ((card I1) + 3)) ';' (((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA)) by SCMFSA6A:29
.= (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:15
.= a =0_goto ((card I1) + 3) by COMPOS_1:58 ;
:: 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 (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 (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:11
.= ((card I1) + 1) + 4 by SCMFSA8A:15
.= ((card I1) + 3) + 2 ;
hence 0 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by AFINSQ_1:66; :: thesis: ( (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (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:62
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:99
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by CARD_1:62 ;
then card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = (card I1) + (3 + 2) by A5;
hence (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by SCMFSA8C:83; :: 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:6;
hence (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by AFINSQ_1:66; :: 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: for p being Instruction-Sequence of SCM+FSA st ss . (intloc 0) = 1 & ss . a = k + 1 & ss . a > 0 holds
( (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
let pp be Instruction-Sequence of SCM+FSA; :: thesis: ( ss . (intloc 0) = 1 & ss . a = k + 1 & ss . a > 0 implies ( (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
assume ss . (intloc 0) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
set s2 = Initialized ss;
set p2 = pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))));
A7: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) c= pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:25;
set s1 = Initialized ss;
set p1 = pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))));
assume A8: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
A9: Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)) = Following ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss)))))) by EXTPRO_1:3
.= Exec ((CurInstr ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss)))))) ;
set s3 = Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1));
set p3 = pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))));
assume A10: ss . a > 0 ; :: thesis: ( (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
A11: ( I1 is_closed_onInit ss,pp & I1 is_halting_onInit ss,pp ) by Th35, Th36;
then A12: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit ss,pp by A10, Th45;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, A11, Th45;
then A13: Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)) = Exec ((goto 0),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss)))))) by A12, A9, Th71;
A14: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, A11, Th45;
A15: card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:11
.= ((card I1) + 1) + 4 by SCMFSA8A:15
.= ((card I1) + 3) + 2 ;
A16: 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:62
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:99
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by CARD_1:62 ;

A17: now

A18: I1 is_halting_onInit ss,pp by Th36;
then A19: I1 is_halting_on Initialized ss,pp by Th41;
I1 is_closed_onInit ss,pp by Th35;
then IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),pp,ss) = (IExec (I1,pp,ss)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A10, A18, Th46;
then A20: (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),pp,ss)) . a = (IExec (I1,pp,ss)) . a by SCMFSA_3:3;

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

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

end;

consider Is being State of SCM+FSA such that
A21: Is = Initialized (Initialized ss) ;
A22: Is = (Initialized ss) +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by A21, FUNCT_4:93
.= ((Initialized ss) +* (Initialize ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= Initialize (Initialized ss) by FUNCT_4:93 ;
I1 is_closed_onInit ss,pp by Th35;
then A23: I1 is_closed_on Initialized ss,pp by Th40;
I1 is_halting_onInit ss,pp by Th36;
then A24: I1 is_halting_on Initialized ss,pp 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,pp by A23, A24, SCMFSA8B:15;
thus Initialized (Initialized ss) = Initialized ss ; :: thesis: ( (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 )

A28: now

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

end;

then (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (Comput ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is)))) . a
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),pp,ss)) . a by A26, A22, SCMFSA8C:58 ;
hence (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (Comput ((pp +* I1),(Initialize (Initialized ss)),(LifeSpan ((pp +* I1),(Initialize (Initialized ss)))))) . a by A19, A20, SCMFSA8C:58
.= (ss . a) - 1 by A1, Th64 ;
:: thesis: (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1
A29: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on Initialized ss,pp by A25, A23, A24, SCMFSA8B:15;
(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = (Comput ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is)))) . (intloc 0) by A28
.= 1 by A26, A29, A22, SCMFSA8C:67 ;
hence (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 ; :: thesis: verum

end;

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

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

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

take m = (((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1) + 1; :: thesis: ( IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),m)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A32: CurInstr ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) = (pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) . 0 by A30, PBOOLE:143
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 by A17, A7, GRFUNC_1:2
.= a =0_goto ((card I1) + 3) by A3, FUNCT_4:105 ;
A33: Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)) = Following ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card I1) + 3)),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) by A32 ;
then IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1))) = (card I1) + 3 by A8, A17, A31, SCMFSA_2:70;
then A34: CurInstr ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)))) = (pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) . ((card I1) + 3) by PBOOLE:143
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . ((card I1) + 3) by A17, A7, GRFUNC_1:2
.= goto (card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A3, FUNCT_4:105 ;
Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),m) = Following ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)))) by A34 ;
hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),m)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by SCMFSA_2:69; :: thesis: for n being Element of NAT st n < m holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),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 ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume n < m ; :: thesis: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
then n <= ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1 by NAT_1:13;
then A35: ( n <= (LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1 or n = ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1 ) by NAT_1:8;

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

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

A37: ( I1 is_closed_onInit ss,pp & I1 is_halting_onInit ss,pp ) by Th35, Th36;
then A38: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, Th45;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit ss,pp by A10, A37, Th45;
then A39: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) = IC (Comput ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss),n)) by A36, A38, Th68;
IC (Comput ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A38, Def4;
hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A39, FUNCT_4:99; :: thesis: verum

end;

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

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

end;

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

hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A8, A17, A31, A33, SCMFSA_2:70; :: thesis: verum

end;

end;

end;

end;

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

consider Is3 being State of SCM+FSA such that
A41: Is3 = Initialized (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) ;
consider m0 being Element of NAT such that
A44: IC (Comput (((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Is3 +* (Initialize ((intloc 0) .--> 1))),m0)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) and
A45: for n being Element of NAT st n < m0 holds
IC (Comput (((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized Is3),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A6, A40, A8, A17, A41;
take m = ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + m0; :: thesis: ( IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),m)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A46: Initialized (Initialized (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) = Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)) by A30, A17, SCMFSA6A:37;
A47: (pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:25, FUNCT_4:98;
hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),m)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A41, A44, A46, EXTPRO_1:4; :: thesis: for n being Element of NAT st n < m holds
IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),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 ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume A48: n < m ; :: thesis: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A49: ( I1 is_closed_onInit ss,pp & I1 is_halting_onInit ss,pp ) by Th35, Th36;
then A50: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, Th45;
A51: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit ss,pp by A10, A49, Th45;

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

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

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

end;

suppose A53: (LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1 <= n ; :: thesis: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),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 ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) ;
n - ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) >= 0 by A53, XREAL_1:48;
then A55: mm = n - ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) by A54, XREAL_0:def 2;
mm + ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) = n by A53, A54, XREAL_1:235;
then A56: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) = IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))),mm)) by EXTPRO_1:4;
m0 = m - ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) ;
then mm < m0 by A48, A55, XREAL_1:9;
hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A41, A45, A46, A47, A56; :: thesis: verum

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,p )
assume A58: s . a > 0 ; :: thesis: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,p
then reconsider sa = s . a as Element of NAT by INT_1:3;
A59: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A59, A2);
then B60: S₁[sa] ;
X4: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
IC <> intloc 0 by SCMFSA_2:56;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by X4, TARSKI:def 1;
then X1: (Initialize s) . (intloc 0) = 1 by A57, FUNCT_4:11;
IC in dom (Start-At (0,SCM+FSA)) by X4, TARSKI:def 1;
then X2: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then X3: dom (Start-At (0,SCM+FSA)) misses dom ((intloc 0) .--> 1) by X4, SCMFSA_2:56, ZFMISC_1:11;
Initialized s = s +* ((Start-At (0,SCM+FSA)) +* ((intloc 0) .--> 1)) by X3, FUNCT_4:35
.= (Initialize s) +* ((intloc 0) .--> 1) by FUNCT_4:14
.= ((Initialize s) +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) by X3, FUNCT_4:115
.= Initialized (Initialize s) by FUNCT_4:14
.= Initialize s by X1, X2, SCMFSA6A:37 ;
then ex k being Element of NAT st
( IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize s),k)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize s),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) by B60, A57, A58;
hence loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,p by SCMFSA8A:def 2; :: thesis: verum