let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s & I is_halting_on Initialized s holds
for k being Element of NAT st k <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) holds
( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k, Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) <> halt SCM+FSA )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on Initialized s & I is_halting_on Initialized s implies for k being Element of NAT st k <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) holds
( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k, Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) <> halt SCM+FSA ) )
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: ( not I is_halting_on Initialized s or for k being Element of NAT st k <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) holds
( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k, Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) <> halt SCM+FSA ) )

A3: now

let k be Element of NAT ; :: thesis: ( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k, Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k equal_outside NAT implies not 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 )
( 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: not 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
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: contradiction
hence contradiction by A6, SCMFSA6A:18; :: thesis: verum

end;

assume A7: I is_halting_on Initialized s ; :: thesis: for k being Element of NAT st k <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) holds
( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k, Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) <> halt SCM+FSA )

now

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: ( ( 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 ) & k + 1 <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) implies ( 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 & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA ) )
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: ( k + 1 <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) implies ( 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 & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA ) )
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 AMI_1:14
.= 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: ( 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 & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA )
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, AMI_1:def 46;
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 AMI_1:14
.= 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: CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA
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: verum

end;

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

now

assume 0 <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) ; :: thesis: ( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),0 , Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),0 equal_outside NAT & CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),0 ) <> halt SCM+FSA )
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 AMI_1:13;
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: CurInstr (ProgramPart (s +* (Initialized (Directed I)))),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),0 ) <> halt SCM+FSA
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: verum

end;

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