let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
( Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),k) <> halt SCM+FSA )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on Initialize s & I is_halting_on Initialize s implies for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
( Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),k) <> halt SCM+FSA ) )
assume A1: I is_closed_on Initialize s ; :: thesis: ( not I is_halting_on Initialize s or for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
( Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),k) <> halt SCM+FSA ) )
assume A2: I is_halting_on Initialize s ; :: thesis: for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
( Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),k) <> halt SCM+FSA )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (Directed I));
A3: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by Th13;

A4: now

let k be Element of NAT ; :: thesis: ( Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT implies not CurInstr (Computation (s +* (Initialized (Directed I))),k) = halt SCM+FSA )
assume A5: Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT ; :: thesis: not CurInstr (Computation (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 A6: Directed I c= Computation (s +* (Initialized (Directed I))),k by AMI_1:81;
dom (Directed I) = dom I by FUNCT_4:105;
then A7: IC (Computation (s +* (Initialized I)),k) in dom (Directed I) by A1, A3, SCMFSA7B:def 7;
A8: CurInstr (Computation (s +* (Initialized (Directed I))),k) = (Computation (s +* (Initialized (Directed I))),k) . (IC (Computation (s +* (Initialized I)),k)) by A5, AMI_1:121
.= (Directed I) . (IC (Computation (s +* (Initialized I)),k)) by A6, A7, GRFUNC_1:8 ;
assume A9: CurInstr (Computation (s +* (Initialized (Directed I))),k) = halt SCM+FSA ; :: thesis: contradiction
CurInstr (Computation (s +* (Initialized (Directed I))),k) in rng (Directed I) by A7, A8, FUNCT_1:def 5;
hence contradiction by A9, SCMFSA6A:18; :: thesis: verum

end;

A10: now

assume 0 <= LifeSpan (s +* (Initialized I)) ; :: thesis: ( Computation (s +* (Initialized I)),0 , Computation (s +* (Initialized (Directed I))),0 equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),0 ) <> halt SCM+FSA )
A11: ( Computation (s +* (Initialized I)),0 = s +* (Initialized I) & Computation (s +* (Initialized (Directed I))),0 = s +* (Initialized (Directed I)) ) by AMI_1:13;
hence Computation (s +* (Initialized I)),0 , Computation (s +* (Initialized (Directed I))),0 equal_outside NAT by SCMFSA6A:53; :: thesis: CurInstr (Computation (s +* (Initialized (Directed I))),0 ) <> halt SCM+FSA
thus CurInstr (Computation (s +* (Initialized (Directed I))),0 ) <> halt SCM+FSA by A4, A11, SCMFSA6A:53; :: thesis: verum

end;

A12: now

let k be Element of NAT ; :: thesis: ( ( k <= LifeSpan (s +* (Initialized I)) implies Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT ) & k + 1 <= LifeSpan (s +* (Initialized I)) implies ( Computation (s +* (Initialized I)),(k + 1), Computation (s +* (Initialized (Directed I))),(k + 1) equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA ) )
assume A13: ( k <= LifeSpan (s +* (Initialized I)) implies Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT ) ; :: thesis: ( k + 1 <= LifeSpan (s +* (Initialized I)) implies ( Computation (s +* (Initialized I)),(k + 1), Computation (s +* (Initialized (Directed I))),(k + 1) equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA ) )
assume A14: k + 1 <= LifeSpan (s +* (Initialized I)) ; :: thesis: ( Computation (s +* (Initialized I)),(k + 1), Computation (s +* (Initialized (Directed I))),(k + 1) equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA )
A15: k + 0 < k + 1 by XREAL_1:8;
then A16: k < LifeSpan (s +* (Initialized I)) by A14, XXREAL_0:2;
( 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 A17: I c= Computation (s +* (Initialized I)),k by AMI_1:81;
( 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 A18: Directed I c= Computation (s +* (Initialized (Directed I))),k by AMI_1:81;
A19: IC (Computation (s +* (Initialized I)),k) in dom I by A1, A3, SCMFSA7B:def 7;
A20: dom I c= dom (Directed I) by FUNCT_4:105;
A21: CurInstr (Computation (s +* (Initialized I)),k) = I . (IC (Computation (s +* (Initialized I)),k)) by A17, A19, GRFUNC_1:8;
s +* (Initialized I) is halting by A2, A3, SCMFSA7B:def 8;
then I . (IC (Computation (s +* (Initialized I)),k)) <> halt SCM+FSA by A16, A21, AMI_1:def 46;
then A22: CurInstr (Computation (s +* (Initialized I)),k) = (Directed I) . (IC (Computation (s +* (Initialized I)),k)) by A21, FUNCT_4:111
.= (Computation (s +* (Initialized (Directed I))),k) . (IC (Computation (s +* (Initialized I)),k)) by A18, A19, A20, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (Directed I))),k) by A13, A14, A15, AMI_1:121, XXREAL_0:2 ;
A23: Computation (s +* (Initialized I)),(k + 1) = Following (Computation (s +* (Initialized I)),k) by AMI_1:14
.= Exec (CurInstr (Computation (s +* (Initialized I)),k)),(Computation (s +* (Initialized I)),k) ;
X: Computation (s +* (Initialized (Directed I))),(k + 1) = Following (Computation (s +* (Initialized (Directed I))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s +* (Initialized (Directed I))),k)),(Computation (s +* (Initialized (Directed I))),k) ;
hence Computation (s +* (Initialized I)),(k + 1), Computation (s +* (Initialized (Directed I))),(k + 1) equal_outside NAT by A13, A14, A15, A22, A23, SCMFSA6A:32, XXREAL_0:2; :: thesis: CurInstr (Computation (s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA
thus CurInstr (Computation (s +* (Initialized (Directed I))),(k + 1)) <> halt SCM+FSA by A4, A13, A14, A15, A22, A23, X, SCMFSA6A:32, XXREAL_0:2; :: thesis: verum

end;

defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan (s +* (Initialized I)) implies ( Computation (s +* (Initialized I)),$1, Computation (s +* (Initialized (Directed I))),$1 equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),$1) <> halt SCM+FSA ) );
A24: S₁[ 0 ] by A10;
A25: for k being Element of NAT st S₁[k] holds
S₁[k + 1] by A12;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A25); :: thesis: verum