let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) & ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
let s be State of SCM+FSA ; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) & ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s ) )
assume A1: I is_closed_on s ; :: thesis: ( not I is_halting_on s or ( IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) & ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s ) )
card (Stop SCM+FSA ) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA )) = (card I) + 1 by SCMFSA6A:61;
then card I < card (I ';' (Stop SCM+FSA )) by NAT_1:13;
then A2: card I in dom (I ';' (Stop SCM+FSA )) by AFINSQ_1:70;
A3: ProgramPart (Relocated (Stop SCM+FSA ),(card I)) c= Relocated (Stop SCM+FSA ),(card I) by RELAT_1:88;
x: 0 in dom (Stop SCM+FSA ) by COMPOS_1:45;
A4: dom (ProgramPart (Stop SCM+FSA )) = dom (Stop SCM+FSA ) by RELAT_1:209;
then 0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA )) } by x;
then 0 + (card I) in dom (Reloc (ProgramPart (Stop SCM+FSA )),(card I)) by AMISTD_2:70;
then A5: 0 + (card I) in dom (ProgramPart (Relocated (Stop SCM+FSA ),(card I))) by AMISTD_2:69;
set s2 = s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
set s1 = s +* (I +* (Start-At 0 ,SCM+FSA ));
x: 0 in dom (Stop SCM+FSA ) by COMPOS_1:45;
y: (Stop SCM+FSA ) . 0 = halt SCM+FSA by AFINSQ_1:38;
assume A6: I is_halting_on s ; :: thesis: ( IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) & ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
then A7: IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) by A1, Th42;
I ';' (Stop SCM+FSA ) c= (I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) by Th9;
then dom (I ';' (Stop SCM+FSA )) c= dom ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
then A8: (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . (card I) = ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) . (card I) by A2, FUNCT_4:14
.= (I ';' (Stop SCM+FSA )) . (card I) by A2, SCMFSA6B:7
.= (ProgramPart (Relocated (Stop SCM+FSA ),(card I))) . (card I) by A5, FUNCT_4:14
.= (Relocated (Stop SCM+FSA ),(card I)) . (0 + (card I)) by A5, A3, GRFUNC_1:8
.= IncAddr (halt SCM+FSA ),(card I) by A4, y, x, AMISTD_2:76
.= halt SCM+FSA by SCMFSA_4:8 ;
DataPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) by A1, A6, Th42;
hence ( IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) ) by A1, A6, A7, Th36; :: thesis: ( ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
Y: (ProgramPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) /. (IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) = (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . (IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) by COMPOS_1:38;
TX: ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) by AMI_1:123;
A9: CurInstr (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . (card I) by A1, A6, A7, Th36, Y, TX
.= halt SCM+FSA by A8, AMI_1:54 ;
hence A10: ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by AMI_1:146; :: thesis: ( LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )

A11: now

let k be Element of NAT ; :: thesis: ( k <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) implies IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) in dom (I ';' (Stop SCM+FSA )) )
assume A12: k <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) in dom (I ';' (Stop SCM+FSA ))
then IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k) by A1, A6, Th35, COMPOS_1:24;
then A13: IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) by A1, A6, A12, Th42;
( IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I & dom I c= dom (I ';' (Stop SCM+FSA )) ) by A1, SCMFSA6A:56, SCMFSA7B:def 7;
hence IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) in dom (I ';' (Stop SCM+FSA )) by A13; :: thesis: verum

end;

defpred S₁[ Nat] means ( ( LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) < $1 implies IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),$1) = card I ) & IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),$1) in dom (I ';' (Stop SCM+FSA )) );
card (Stop SCM+FSA ) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA )) = (card I) + 1 by SCMFSA6A:61;
then A14: (card I) + 0 < card (I ';' (Stop SCM+FSA )) by XREAL_1:8;
then A15: card I in dom (I ';' (Stop SCM+FSA )) by AFINSQ_1:70;

A16: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[b₁ + 1] )
assume A17: S₁[k] ; :: thesis: S₁[b₁ + 1]

per cases ( k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) or k = LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) or k > LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) ) by XXREAL_0:1;

suppose k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: S₁[b₁ + 1]

then k + 1 <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) by NAT_1:13;
hence S₁[k + 1] by A11; :: thesis: verum

end;

suppose k = LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: S₁[b₁ + 1]

hence S₁[k + 1] by A1, A6, A7, A15, Th36; :: thesis: verum

end;

suppose A18: k > LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: S₁[b₁ + 1]

A19: now

assume k + 1 > LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(k + 1)) = card I
Y: (ProgramPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k)) /. (IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k)) = (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . (IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k)) by COMPOS_1:38;
A20: CurInstr (ProgramPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA by A8, A17, A18, Y, AMI_1:54;
T: ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) by AMI_1:123;
thus IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(k + 1)) = IC (Following (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k)) by AMI_1:14
.= card I by A17, A18, A20, T, AMI_1:def 8 ; :: thesis: verum

end;

k + 1 > k + 0 by XREAL_1:8;
hence S₁[k + 1] by A14, A18, A19, AFINSQ_1:70, XXREAL_0:2; :: thesis: verum

end;

end;

end;

now

let k be Element of NAT ; :: thesis: ( k < (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 implies CurInstr (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) <> halt SCM+FSA )
TY: ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k) by AMI_1:123;
TU: ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) by AMI_1:123;
assume k < (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 ; :: thesis: CurInstr (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) <> halt SCM+FSA
then A21: k <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) by NAT_1:13;
then CurInstr (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k) <> halt SCM+FSA by A1, A6, Th35;
hence CurInstr (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) <> halt SCM+FSA by A1, A6, A21, Th42, TY, TU; :: thesis: verum

end;

then for k being Element of NAT st CurInstr (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA holds
(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 <= k ;
hence LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 by A9, A10, AMI_1:def 46; :: thesis: ( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
A22: S₁[ 0 ] by A11, NAT_1:2;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A22, A16);
hence I ';' (Stop SCM+FSA ) is_closed_on s by SCMFSA7B:def 7; :: thesis: I ';' (Stop SCM+FSA ) is_halting_on s
thus I ';' (Stop SCM+FSA ) is_halting_on s by A10, SCMFSA7B:def 8; :: thesis: verum