let s2 be State of SCM+FSA ; :: thesis: not s2 +* (IC s2),(goto (IC s2)) is halting
set s1 = s2 +* (IC s2),(goto (IC s2));
A1: IC SCM+FSA <> IC s2 by AMI_1:48;
A2: IC s2 in dom s2 by AMI_1:115;
defpred S₁[ Element of NAT ] means IC (Computation (s2 +* (IC s2),(goto (IC s2))),$1) = IC (s2 +* (IC s2),(goto (IC s2)));
A3: S₁[ 0 ] by AMI_1:13;
A4: IC (s2 +* (IC s2),(goto (IC s2))) = IC s2 by A1, FUNCT_7:34;

A5: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A6: CurInstr (Computation (s2 +* (IC s2),(goto (IC s2))),n) = (s2 +* (IC s2),(goto (IC s2))) . (IC (s2 +* (IC s2),(goto (IC s2)))) by AMI_1:54
.= goto (IC s2) by A2, A4, FUNCT_7:33 ;
IC (Computation (s2 +* (IC s2),(goto (IC s2))),(n + 1)) = IC (Following (Computation (s2 +* (IC s2),(goto (IC s2))),n)) by AMI_1:14
.= IC (s2 +* (IC s2),(goto (IC s2))) by A4, A6, SCMFSA_2:95 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A7: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A5);
let n be Element of NAT ; :: according to AMI_1:def 20 :: thesis: not CurInstr (Computation (s2 +* (IC s2),(goto (IC s2))),n) = halt SCM+FSA
CurInstr (Computation (s2 +* (IC s2),(goto (IC s2))),n) = (Computation (s2 +* (IC s2),(goto (IC s2))),n) . (IC (s2 +* (IC s2),(goto (IC s2)))) by A7
.= (s2 +* (IC s2),(goto (IC s2))) . (IC (s2 +* (IC s2),(goto (IC s2)))) by AMI_1:54
.= goto (IC s2) by A2, A4, FUNCT_7:33 ;
hence not CurInstr (Computation (s2 +* (IC s2),(goto (IC s2))),n) = halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124; :: thesis: verum