let s2 be State of SCM+FSA ; :: thesis: not ProgramPart (s2 +* (IC s2),(goto (IC s2))) halts_on s2 +* (IC s2),(goto (IC s2))
set s1 = s2 +* (IC s2),(goto (IC s2));
defpred S₁[ Nat] means IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),$1) = IC (s2 +* (IC s2),(goto (IC s2)));
IC SCM+FSA <> IC s2 by COMPOS_1:3;
then A1: IC (s2 +* (IC s2),(goto (IC s2))) = IC s2 by FUNCT_7:34;
A2: IC s2 in dom s2 by COMPOS_1:22;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
Y: (ProgramPart (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)) /. (IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)) = (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) . (IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)) by COMPOS_1:38;
T: ProgramPart (s2 +* (IC s2),(goto (IC s2))) = ProgramPart (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) by AMI_1:123;
assume S₁[n] ; :: thesis: S₁[n + 1]
then A4: CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) = (s2 +* (IC s2),(goto (IC s2))) . (IC (s2 +* (IC s2),(goto (IC s2)))) by Y, AMI_1:54
.= goto (IC s2) by A2, A1, FUNCT_7:33 ;
IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),(n + 1)) = IC (Following (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)) by AMI_1:14
.= IC (s2 +* (IC s2),(goto (IC s2))) by A1, A4, T, SCMFSA_2:95 ;
hence S₁[n + 1] ; :: thesis: verum

end;

let n be Nat; :: according to AMI_1:def 20 :: thesis: ( not IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) in proj1 (ProgramPart (s2 +* (IC s2),(goto (IC s2)))) or not CurInstr (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) = halt SCM+FSA )
A5: S₁[ 0 ] by AMI_1:13;
assume IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) in dom (ProgramPart (s2 +* (IC s2),(goto (IC s2)))) ; :: thesis: not CurInstr (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) = halt SCM+FSA
reconsider n = n as Element of NAT by ORDINAL1:def 13;
ProgramPart (s2 +* (IC s2),(goto (IC s2))) = ProgramPart (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) by AMI_1:123;
then Y: (ProgramPart (s2 +* (IC s2),(goto (IC s2)))) /. (IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)) = (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) . (IC (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n)) by COMPOS_1:38;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A3);
then CurInstr (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) = (Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) . (IC (s2 +* (IC s2),(goto (IC s2)))) by Y
.= (s2 +* (IC s2),(goto (IC s2))) . (IC (s2 +* (IC s2),(goto (IC s2)))) by AMI_1:54
.= goto (IC s2) by A2, A1, FUNCT_7:33 ;
then CurInstr (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124;
hence not CurInstr (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(Comput (ProgramPart (s2 +* (IC s2),(goto (IC s2)))),(s2 +* (IC s2),(goto (IC s2))),n) = halt SCM+FSA ; :: thesis: verum