let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
( 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 & 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 )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on s & I is_halting_on s implies for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
( 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 & 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 ) )
assume that
A1: I is_closed_on s and
A2: I is_halting_on s ; :: thesis: for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
( 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 & 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 )
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 (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 (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed 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) <> halt SCM+FSA ) );

A3: now

let k be Element of NAT ; :: thesis: ( 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 implies not 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 )
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 AMI_1:150;
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: not 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
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 AMI_1:121, Y
.= (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: contradiction
hence contradiction by A6, SCMFSA6A:18; :: thesis: verum

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: ( ( k <= LifeSpan (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 ) & k + 1 <= LifeSpan (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 + 1), Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(k + 1) equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed 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)) <> halt SCM+FSA ) )
assume A9: ( k <= LifeSpan (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: ( k + 1 <= LifeSpan (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 + 1), Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(k + 1) equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed 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)) <> halt SCM+FSA ) )
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:144;
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 AMI_1:14
.= 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 AMI_1:150;
( 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 (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) = I . (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) by A11, GRFUNC_1:8, Y;
( 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 AMI_1:150;
assume A15: k + 1 <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: ( 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 & CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed 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)) <> halt SCM+FSA )
then k < LifeSpan (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, AMI_1:def 46;
then A16: 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) = (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, AMI_1:121, XXREAL_0:2, Y ;
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:144;
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 AMI_1:14
.= 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, A14, A16, A10, SCMFSA6A:32, XXREAL_0:2; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed 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)) <> halt SCM+FSA
thus CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed 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)) <> halt SCM+FSA by A3, A9, A15, A14, A16, A17, A10, SCMFSA6A:32, XXREAL_0:2; :: thesis: verum

end;

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

now

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

end;

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