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

A3: now

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

end;

assume A7: I is_halting_on Initialized s ; :: thesis:

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

end;

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

assume 0 <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) ; :: thesis:
A20: ( Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),0) = s +* (Initialized I) & Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),0) = s +* (Initialized (Directed I)) ) by EXTPRO_1:3;
hence Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),0), Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),0) equal_outside NAT by SCMFSA6A:53; :: thesis:
thus CurInstr ((ProgramPart (s +* (Initialized (Directed I)))),(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),0))) <> halt SCM+FSA by A3, A20, SCMFSA6A:53; :: thesis:

end;

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