let s be State of SCM+FSA ; :: thesis:
set A = NAT ;
let I be parahalting good Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
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 destroysdestroy a ; :: thesis:
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A3: S₁[k] ; :: thesis:
let ss be State of SCM+FSA ; :: thesis:
assume A4: ss . (intloc 0 ) = 1 ; :: thesis:
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:
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:
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 AMI_1:14
.= 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:

thus 0 in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A19, A18, AFINSQ_1:70; :: thesis:
((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:

end;

A20: dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) misses dom (Start-At 0 ,SCM+FSA ) by SF_MASTR:64;
thus intloc 0 in dom ss by SCMFSA_2:66; :: thesis:
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 )) ;
Initialized ss = (ss +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) by SCMFSA6A:def 4;
then 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 (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:

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:
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:

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:

A31: now

InsCode (a =0_goto ((card I1) + 3)) = 7 by SCMFSA_2:48;
then A32: (Macro (a =0_goto ((card I1) + 3))) . 0 <> halt SCM+FSA by SCMFSA6B:33, SCMFSA_2:124;
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 SCMFSA6B:33 ;
:: thesis:
hence (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124; :: thesis:
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:
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:
hence (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124; :: thesis:

hereby :: thesis:

((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:

end;

end;

hereby :: thesis:

per cases ;

suppose A35: k = 0 ; :: thesis:

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:
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 AMI_1:14
.= 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 AMI_1:14
.= 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:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume n < m ; :: thesis:
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 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:

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:

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:

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:

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:

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:

end;

end;

end;

end;

suppose A45: k > 0 ; :: thesis:

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 SF_MASTR:64;
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:
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, AMI_1:51; :: thesis:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume A54: n < m ; :: thesis:
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 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:

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:

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:

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 AMI_1:51;
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:

end;

end;

end;

end;

end;

end;

end;

assume A64: s . (intloc 0 ) = 1 ; :: thesis:
assume A65: s . a > 0 ; :: thesis:
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: