let s be State of SCM+FSA; :: thesis:
let I be Program of SCM+FSA; :: thesis:
assume that
A1: I is_closed_on s and
A2: I is_halting_on s ; :: thesis:
set s2 = s +* ((Directed I) +* (Start-At (0,SCM+FSA)));
set s1 = s +* (I +* (Start-At (0,SCM+FSA)));
defpred S₁[ Nat] means ( $1 <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) implies ( Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1), Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),$1) equal_outside NAT & 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)))),$1))) <> halt SCM+FSA ) );

A3: now

let k be Element of NAT ; :: thesis:
dom (Directed I) = dom I by FUNCT_4:105;
then A4: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom (Directed I) by A1, SCMFSA7B:def 7;
( Directed I c= (Directed I) +* (Start-At (0,SCM+FSA)) & (Directed I) +* (Start-At (0,SCM+FSA)) c= s +* ((Directed I) +* (Start-At (0,SCM+FSA))) ) by Th9, FUNCT_4:26;
then Directed I c= s +* ((Directed I) +* (Start-At (0,SCM+FSA))) by XBOOLE_1:1;
then A5: Directed I c= Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k) by AMI_1:81;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed 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))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed 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 COMPOS_1:38;
assume Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k) equal_outside NAT ; :: thesis:
then CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (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 Y, COMPOS_1:24
.= (Directed I) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) by A5, A4, GRFUNC_1:8 ;
then A6: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) in rng (Directed I) by A4, FUNCT_1:def 5;
assume CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) = halt SCM+FSA ; :: thesis:
hence contradiction by A6, SCMFSA6A:18; :: thesis:

end;

now

A7: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) halts_on s +* (I +* (Start-At (0,SCM+FSA))) by A2, SCMFSA7B:def 8;
A8: dom I c= dom (Directed I) by FUNCT_4:105;
let k be Element of NAT ; :: thesis:
assume A9: ( k <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) implies Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k) equal_outside NAT ) ; :: thesis:
T: 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;
A10: Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(k + 1)) = Following ((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))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by T ;
A11: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by A1, SCMFSA7B:def 7;
Y: (ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (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 COMPOS_1:38;
TX: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) by AMI_1:123;
( I c= I +* (Start-At (0,SCM+FSA)) & I +* (Start-At (0,SCM+FSA)) c= s +* (I +* (Start-At (0,SCM+FSA))) ) by Th9, FUNCT_4:26;
then I c= s +* (I +* (Start-At (0,SCM+FSA))) by XBOOLE_1:1;
then I c= Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k) by AMI_1:81;
then A12: CurInstr ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) = I . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) by A11, Y, TX, GRFUNC_1:8;
( Directed I c= (Directed I) +* (Start-At (0,SCM+FSA)) & (Directed I) +* (Start-At (0,SCM+FSA)) c= s +* ((Directed I) +* (Start-At (0,SCM+FSA))) ) by Th9, FUNCT_4:26;
then Directed I c= s +* ((Directed I) +* (Start-At (0,SCM+FSA))) by XBOOLE_1:1;
then A13: Directed I c= Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k) by AMI_1:81;
A14: k + 0 < k + 1 by XREAL_1:8;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed 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))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed 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 COMPOS_1:38;
assume A15: k + 1 <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) ; :: thesis:
then k < LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) by A14, XXREAL_0:2;
then I . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) <> halt SCM+FSA by A12, A7, EXTPRO_1:def 14;
then A16: CurInstr ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) = (Directed I) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) by A12, FUNCT_4:111
.= (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (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 A13, A11, A8, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by A9, A15, A14, Y, COMPOS_1:24, XXREAL_0:2 ;
T: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) by AMI_1:123;
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 + 1))) by AMI_1:123;
A17: Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)) = Following ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))) by T ;
hence Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)), Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(k + 1)) equal_outside NAT by A9, A15, TX, A14, A16, A10, SCMFSA6A:32, XXREAL_0:2; :: thesis:
thus 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 + 1)))) <> halt SCM+FSA by A3, A9, A15, A14, A16, A17, TX, TY, A10, SCMFSA6A:32, XXREAL_0:2; :: thesis:

end;

then A18: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;

now

assume 0 <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) ; :: thesis:
A19: ( Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0) = s +* (I +* (Start-At (0,SCM+FSA))) & Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),0) = s +* ((Directed I) +* (Start-At (0,SCM+FSA))) ) by EXTPRO_1:3;
hence Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0), Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),0) equal_outside NAT by Th14; :: thesis:
thus 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)))),0))) <> halt SCM+FSA by A3, A19, Th14; :: thesis:

end;

then A20: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A20, A18); :: thesis: