let s be State of SCM+FSA; :: thesis: for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st 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
set A = NAT ;
let I be parahalting good 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 parahalting 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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (s . a) - 1 & (Comput ((ProgramPart (s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: 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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
assume A4: ss . (intloc 0) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
set s2 = ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)));
set s1 = ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)));
assume A5: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) ) )
set s3 = Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1));
assume A6: ss . a > 0 ; :: thesis: ( (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
T: ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
A7: Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)) = Following ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))))))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))))))) by T ;
A8: I1 is_halting_on ss by SCMFSA7B:25;
A9: I1 is_closed_on ss by SCMFSA7B:24;
then A10: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss by A6, A8, SCMFSA8B:18;
A11: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on ss by A6, A9, A8, SCMFSA8B:18;
A12: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss by A6, A9, A8, SCMFSA8B:18;
then A13: IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) = (Exec ((goto 0),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))))))) . (IC SCM+FSA) by A11, A7, Lm2, T
.= 0 by SCMFSA_2:95 ;
A14: Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)) = Exec ((goto 0),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))))))) by A12, A11, A7, Lm2, T;

A15: now

A16: I1 is_halting_on Initialized ss by SCMFSA7B:25;
I1 is_closed_on Initialized ss by SCMFSA7B:24;
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 A6, A16, SCMFSA8B:19;
then A17: (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),ss)) . a = (IExec (I1,ss)) . a by SCMFSA_3:11;
A18: 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 ;
A19: 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:105
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) ;

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

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

A20: dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
thus intloc 0 in dom ss by SCMFSA_2:66; :: thesis: ( (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (ss . a) - 1 & (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 )
then A21: ss +* ((intloc 0) .--> 1) = ss by A4, FUNCT_7:111;
A22: I1 is_closed_on Initialized ss by SCMFSA7B:24;
A23: I1 is_halting_on Initialized ss by SCMFSA7B:25;
A24: (Initialized ss) . a > 0 by A6, SCMFSA6C:3;
then A25: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on Initialized ss by A22, A23, SCMFSA8B:18;
A26: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on Initialized ss by A24, A22, A23, SCMFSA8B:18;
consider Is being State of SCM+FSA such that
A27: Is = (Initialized ss) +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))) ;
A28: (Initialized ss) +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))) = (ss +* (Start-At (0,SCM+FSA))) +* ((Start-At (0,SCM+FSA)) +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A21, A20, FUNCT_4:36
.= ((ss +* (Start-At (0,SCM+FSA))) +* (Start-At (0,SCM+FSA))) +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by FUNCT_4:15
.= (ss +* ((Start-At (0,SCM+FSA)) +* (Start-At (0,SCM+FSA)))) +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by FUNCT_4:15
.= ss +* ((Start-At (0,SCM+FSA)) +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:15
.= ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))) by A20, FUNCT_4:36 ;

A29: now

let b be Int-Location ; :: thesis: (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . b = (Comput ((ProgramPart Is),Is,(LifeSpan ((ProgramPart Is),Is)))) . b
(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . b = (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))))) . b by A14, SCMFSA_2:95;
hence (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . b = (Comput ((ProgramPart Is),Is,(LifeSpan ((ProgramPart Is),Is)))) . b by A11, A10, A28, A27, Th109, SCMFSA10:92; :: thesis: verum

end;

then (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 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 A27, A25, Th87 ;
hence (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 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 A16, A17, Th87
.= (ss . a) - 1 by A1, Th98 ;
:: thesis: (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1
A30: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good by Th115;
(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = (Comput ((ProgramPart Is),Is,(LifeSpan ((ProgramPart Is),Is)))) . (intloc 0) by A29
.= 1 by A27, A25, A26, A30, Th96 ;
hence (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (intloc 0) = 1 ; :: thesis: verum

end;

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

A31: now

A32: (Macro (a =0_goto ((card I1) + 3))) . 0 <> halt SCM+FSA by COMPOS_1:148;
A33: 0 in dom (Macro (a =0_goto ((card I1) + 3))) by 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 A33, A32, 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)))))) )
A34: 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))))))))
.= 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)))))) ;
then card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) = (card I1) + (3 + 2) by A34, 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 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 A34, 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;

hereby :: thesis: verum

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

suppose A35: k = 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

take m = (((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1) + 1; :: thesis: ( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
Y: (ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) /. (IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) = (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) . (IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) by COMPOS_1:38;
A36: CurInstr ((ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) = (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) . 0 by A13, Y, AMI_1:54
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 by A15, Th26
.= a =0_goto ((card I1) + 3) by A31, FUNCT_4:111 ;
Y: (ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))) /. (IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))) = (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1))) . (IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))) by COMPOS_1:38;
T: ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) by AMI_1:123;
A37: Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)) = Following ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) by EXTPRO_1:4
.= Exec ((a =0_goto ((card I1) + 3)),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) by A36, T ;
then IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1))) = (card I1) + 3 by A5, A15, A35, SCMFSA_2:96;
then A38: CurInstr ((ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))) = (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) . ((card I1) + 3) by Y, AMI_1:54
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . ((card I1) + 3) by A15, Th26
.= goto (card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) by A31, FUNCT_4:111 ;
T: ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1))) by AMI_1:123;
Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),m) = Following ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))) by EXTPRO_1:4
.= Exec ((goto (card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1)))) by A38, T ;
hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume n < m ; :: thesis: IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
then n <= ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1 by NAT_1:13;
then A39: ( n <= (LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1 or n = ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1 ) by NAT_1:8;

per cases ( n <= LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))) or n = (LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1 or n = ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + 1 ) by A39, NAT_1:8;

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

A41: I1 is_halting_on ss by SCMFSA7B:25;
A42: I1 is_closed_on ss by SCMFSA7B:24;
then A43: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss by A6, A41, SCMFSA8B:18;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on ss by A6, A42, A41, SCMFSA8B:18;
then Comput ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),n), Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n) equal_outside NAT by A40, A43, Th109;
then A44: IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),n)) by SCMFSA8A:6;
IC (Comput ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A43, SCMFSA7B:def 7;
hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A44, FUNCT_4:105; :: thesis: verum

end;

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

hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A13, A15; :: thesis: verum

end;

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

hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A5, A15, A35, A37, SCMFSA_2:96; :: thesis: verum

end;

end;

end;

end;

suppose A45: k > 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

consider Is3 being State of SCM+FSA such that
A46: Is3 = Initialized (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) ;
A47: dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then (Initialized (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) = (Initialized (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) +* ((Start-At (0,SCM+FSA)) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by FUNCT_4:36
.= ((Initialized (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) +* (Start-At (0,SCM+FSA))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:15 ;
then A48: (Initialized (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) = ((Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) +* ((IC SCM+FSA) .--> 0)) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A13, A15, Th14;
ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) = ss +* ((Start-At (0,SCM+FSA)) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A47, FUNCT_4:36
.= (ss +* (Start-At (0,SCM+FSA))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:15 ;
then ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) c= Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)) by AMI_1:99, FUNCT_4:26;
then A49: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) c= Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)) by RELAT_1:209;
A50: Is3 . (intloc 0) = 1 by A46, SCMFSA6C:3;
Is3 . a = k by A5, A15, A46, SCMFSA6C:3;
then consider m0 being Element of NAT such that
A51: IC (Comput ((ProgramPart (Is3 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(Is3 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),m0)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) and
A52: for n being Element of NAT st n < m0 holds
IC (Comput ((ProgramPart (Is3 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(Is3 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A3, A45, A50;
take m = ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) + m0; :: thesis: ( IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
T: ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) by AMI_1:123;
IC SCM+FSA in dom (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) by COMPOS_1:9;
then A53: (Initialized (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)))) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))) = (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A13, A48, FUNCT_7:111
.= Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1)) by A49, FUNCT_4:79 ;
hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),m)) = card (ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A46, A51, T, EXTPRO_1:5; :: thesis: for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume A54: n < m ; :: thesis: IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A55: I1 is_halting_on ss by SCMFSA7B:25;
A56: I1 is_closed_on ss by SCMFSA7B:24;
then A57: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on ss by A6, A55, SCMFSA8B:18;
A58: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on ss by A6, A56, A55, SCMFSA8B:18;

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

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

then Comput ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),n), Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n) equal_outside NAT by A57, A58, Th109;
then A59: IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),n)) by SCMFSA8A:6;
IC (Comput ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A57, SCMFSA7B:def 7;
hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A59, FUNCT_4:105; :: thesis: verum

end;

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

consider mm being Element of NAT such that
A61: mm = n -' ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) ;
n - ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) >= 0 by A60, XREAL_1:50;
then A62: mm = n - ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) by A61, XREAL_0:def 2;
T: ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))) by AMI_1:123;
mm + ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) = n by A60, A61, XREAL_1:237;
then A63: IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1))),mm)) by EXTPRO_1:5;
m0 = m - ((LifeSpan ((ProgramPart (ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))) + 1) ;
then mm < m0 by A54, A62, XREAL_1:11;
hence IC (Comput ((ProgramPart (ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(ss +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A46, A52, A53, A63, T; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

assume A64: 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 A65: 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;
A66: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A66, A2);
then S₁[sa] ;
then ex k being Element of NAT st
( IC (Comput ((ProgramPart (s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),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 +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA))))),(s +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) +* (Start-At (0,SCM+FSA)))),n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) by A64, A65;
hence loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s by SCMFSA8A:def 3; :: thesis: verum