let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good parahalting 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 s be State of SCM+FSA; :: thesis: for I being good parahalting 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
set A = NAT ;
let I be good parahalting 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 I2 = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
reconsider I1 = I ';' (SubFrom (a,(intloc 0))) as parahalting Program of SCM+FSA ;
set i = a =0_goto ((card I1) + 3);
defpred S1[ Nat] means for s being State 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)))))))),(Initialize s),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . a = (s . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize s),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize 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)))))))),(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))))))) ) ) );
assume A3: 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 )
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
let ss be State of SCM+FSA; :: thesis: ( ss . (intloc 0) = 1 & ss . a = k + 1 & ss . a > 0 implies ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize 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)))))))),(Initialize 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)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
assume A6: ss . (intloc 0) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize 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)))))))),(Initialize 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)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
set s2 = Initialize ss;
set P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))));
set s1 = Initialize ss;
set P1 = P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))));
A7: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) c= P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:25;
assume A8: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize 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)))))))),(Initialize 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)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
set s3 = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1));
set P3 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))));
A9: (P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:93;
assume A10: ss . a > 0 ; :: thesis: ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize 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)))))))),(Initialize 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)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
A11: Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)) = Following ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss)))))) by EXTPRO_1:3;
A12: I1 is_halting_on ss,P by SCMFSA7B:19;
A13: I1 is_closed_on ss,P by SCMFSA7B:18;
then A14: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A10, A12, SCMFSA8B:15;
A15: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on ss,P by A10, A13, A12, SCMFSA8B:15;
A16: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A10, A13, A12, SCMFSA8B:15;
then A17: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) = (Exec ((goto 0),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))))))) . (IC ) by A15, A11, Lm2
.= 0 by SCMFSA_2:69 ;
A18: Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)) = Exec ((goto 0),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss)))))) by A16, A15, A11, Lm2;
A19: now
A20: I1 is_halting_on Initialized ss,P by SCMFSA7B:19;
B20: I1 is_closed_on Initialized ss,P by SCMFSA7B:18;
IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,ss) = (IExec (I1,P,ss)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A10, A20, B20, SCMFSA8B:16;
then A21: (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,ss)) . a = (IExec (I1,P,ss)) . a by SCMFSA_3:3;
A22: 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 ;
A23: 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))))))))
.= 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)))))) ;
hereby :: thesis: ( intloc 0 in dom ss & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 )
thus 0 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A23, 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 A22, NAT_1:13;
then (card I1) + 3 < card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A23, 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;
thus intloc 0 in dom ss by SCMFSA_2:42; :: thesis: ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 )
then A25: ss +* ((intloc 0) .--> 1) = ss by A6, FUNCT_7:109;
A26: I1 is_closed_on Initialized ss,P by SCMFSA7B:18;
A27: I1 is_halting_on Initialized ss,P by SCMFSA7B:19;
A28: (Initialized ss) . a > 0 by A10, SCMFSA6C:3;
then A29: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on Initialized ss,P by A26, A27, SCMFSA8B:15;
A30: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on Initialized ss,P by A28, A26, A27, SCMFSA8B:15;
consider Is being State of SCM+FSA such that
A31: Is = Initialize (Initialized ss) ;
set IP = P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))));
A32: Initialize (Initialized ss) = Initialize (Initialized ss)
.= ((ss +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= Initialize ss by A25, FUNCT_4:93
.= Initialize ss ;
A33: now
let b be Int-Location ; :: thesis: (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is)))) . b
XX: Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is))) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is))) by A15, A14, A32, A31, Th109;
(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))))) . b by A18, SCMFSA_2:69;
hence (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is)))) . b by A32, A31, XX; :: thesis: verum
end;
then (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is)))) . a
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,ss)) . a by A31, A29, Th87 ;
hence (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (Comput ((P +* I1),((Initialized ss) +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I1),(Initialize (Initialized ss)))))) . a by A20, A21, Th87
.= (ss . a) - 1 by A3, Th98 ;
:: thesis: (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1
A34: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good by Th115;
(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),Is)))) . (intloc 0) by A33
.= 1 by A31, A29, A30, A34, Th96 ;
hence (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 ; :: thesis: verum
end;
hence ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 ) ; :: thesis: ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A35: now
A36: (Macro (a =0_goto ((card I1) + 3))) . 0 <> halt SCM+FSA by COMPOS_1:58;
A37: 0 in dom (Macro (a =0_goto ((card I1) + 3))) by 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 A37, A36, 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)))))) )
A38: 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))))))))
.= 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)))))) ;
then card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = (card I1) + (3 + 2) by A38;
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 Th116; :: 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 A38, 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;
hereby :: thesis: verum
per cases ( k = 0 or k > 0 ) ;
suppose A39: k = 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
take m = (((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1) + 1; :: thesis: ( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A41: CurInstr ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) = (P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) . 0 by A17, PBOOLE:143
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 by A19, A7, GRFUNC_1:2
.= a =0_goto ((card I1) + 3) by A35, FUNCT_4:105 ;
A42: (P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) /. (IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) = (P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) . (IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) by PBOOLE:143;
A43: Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)) = Following ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card I1) + 3)),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) by A41 ;
then A44: CurInstr ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) = (P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) . ((card I1) + 3) by A42, A8, A19, A39, SCMFSA_2:70
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . ((card I1) + 3) by A19, A7, GRFUNC_1:2
.= goto (card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A35, FUNCT_4:105 ;
Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),m) = Following ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) by A44 ;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume n < m ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
then n <= ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 by NAT_1:13;
then A45: ( n <= (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 or n = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 ) by NAT_1:8;
per cases ( n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss)) or n = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 or n = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 ) by A45, NAT_1:8;
suppose A46: n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss)) ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A47: I1 is_halting_on ss,P by SCMFSA7B:19;
A48: I1 is_closed_on ss,P by SCMFSA7B:18;
then A49: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A10, A47, SCMFSA8B:15;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on ss,P by A10, A48, A47, SCMFSA8B:15;
then Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),n) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n) by A46, A49, Th109;
then A50: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) = IC (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) ;
IC (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A49, SCMFSA7B:def 6;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A50, FUNCT_4:99; :: thesis: verum
end;
suppose n = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A17, A19; :: thesis: verum
end;
suppose n = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A8, A19, A39, A43, SCMFSA_2:70; :: thesis: verum
end;
end;
end;
end;
suppose A51: k > 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
consider Is3 being State of SCM+FSA such that
A52: Is3 = Initialized (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) ;
A54: Initialize (Initialized (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) = (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) +* ((IC ) .--> 0) by A17, A19, SCMFSA6A:37;
A56: Is3 . (intloc 0) = 1 by A52, SCMFSA6A:38;
Is3 . a = k by A8, A19, A52, SCMFSA6C:3;
then consider m0 being Element of NAT such that
A57: IC (Comput (((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize Is3),m0)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) and
A58: for n being Element of NAT st n < m0 holds
IC (Comput (((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize Is3),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A5, A51, A56, A9;
take m = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + m0; :: thesis: ( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
XX: IC in dom (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) by MEMSTR_0:2;
A59: Initialize (Initialized (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) = (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) +* ((IC ) .--> 0) by A54
.= (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) +* (Start-At (0,SCM+FSA))
.= Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)) by A17, XX, FUNCT_7:109 ;
thus IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A52, A57, A59, A9, EXTPRO_1:4; :: thesis: for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize 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 ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume A60: n < m ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A61: I1 is_halting_on ss,P by SCMFSA7B:19;
A62: I1 is_closed_on ss,P by SCMFSA7B:18;
then A63: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A10, A61, SCMFSA8B:15;
A64: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on ss,P by A10, A62, A61, SCMFSA8B:15;
per cases ( n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss)) or (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 <= n ) by NAT_1:13;
suppose n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss)) ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
then Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),n) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n) by A63, A64, Th109;
then A65: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) = IC (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) ;
IC (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A63, SCMFSA7B:def 6;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A65, FUNCT_4:99; :: thesis: verum
end;
suppose A66: (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 <= n ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
consider mm being Element of NAT such that
A67: mm = n -' ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) ;
n - ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) >= 0 by A66, XREAL_1:48;
then A68: mm = n - ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) by A67, XREAL_0:def 2;
mm + ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) = n by A66, A67, XREAL_1:235;
then A69: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) = IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))),mm)) by EXTPRO_1:4;
m0 = m - ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) ;
then mm < m0 by A60, A68, XREAL_1:9;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A52, A58, A59, A69, A9; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
assume A70: 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 A71: 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;
A72: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A72, A4);
 then S1[sa] ;
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 A70, A71;
hence loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P by SCMFSA8A:def 2; :: thesis: verum