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 COMPOS_1:117;
then A5: 0 + (card I) in dom (ProgramPart (Relocated ((Stop SCM+FSA),(card I)))) by COMPOS_1:116;
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, COMPOS_1:145
.= (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, COMPOS_1:122
.= 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 EXTPRO_1:30; :: 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 S1[ 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: ( S1[k] implies S1[b1 + 1] )
assume A17: S1[k] ; :: thesis: S1[b1 + 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: S1[b1 + 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 S1[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: S1[b1 + 1]
hence S1[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: S1[b1 + 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 EXTPRO_1:4
.= card I by A17, A18, A20, T, EXTPRO_1:def 3 ; :: thesis: verum
end;
k + 1 > k + 0 by XREAL_1:8;
hence S1[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, EXTPRO_1:def 14; :: thesis: ( I ';' (Stop SCM+FSA) is_closed_on s & I ';' (Stop SCM+FSA) is_halting_on s )
A22: S1[ 0 ] by A11, NAT_1:2;
for k being Element of NAT holds S1[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