let l be Element of NAT ; :: thesis: for s being State of SCM+FSA st IC s = l & s . l = goto l holds
not ProgramPart s halts_on s
let s be State of SCM+FSA; :: thesis: ( IC s = l & s . l = goto l implies not ProgramPart s halts_on s )
assume that
A1: IC s = l and
A2: s . l = goto l ; :: thesis: not ProgramPart s halts_on s
defpred S₁[ Nat] means Comput ((ProgramPart s),s,$1) = s;
A3: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
A4: ( ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) & ( for i being Element of NAT holds (Exec ((goto l),s)) . i = s . i ) ) by AMI_1:def 13, SCMFSA_2:95;
A5: ( IC (Exec ((goto l),s)) = IC s & ( for a being Int-Location holds (Exec ((goto l),s)) . a = s . a ) ) by A1, SCMFSA_2:95;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
assume Comput ((ProgramPart s),s,m) = s ; :: thesis: S₁[m + 1]
hence Comput ((ProgramPart s),s,(m + 1)) = Following ((ProgramPart s),s) by EXTPRO_1:4
.= s by A1, A2, A5, A4, Y, SCMFSA_2:86 ;
:: thesis: verum

end;

let mm be Nat; :: according to EXTPRO_1:def 7 :: thesis: ( not IC (Comput ((ProgramPart s),s,mm)) in proj1 (ProgramPart s) or not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,mm))) = halt SCM+FSA )
reconsider m = mm as Element of NAT by ORDINAL1:def 13;
A6: S₁[ 0 ] by EXTPRO_1:3;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,m)) by AMI_1:123;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A6, A3);
then B7: S₁[m] ;
Z: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
assume IC (Comput ((ProgramPart s),s,mm)) in dom (ProgramPart s) ; :: thesis: not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,mm))) = halt SCM+FSA
CurInstr ((ProgramPart s),s) = goto l by A1, A2, Z;
then X: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,m))),(Comput ((ProgramPart s),s,m))) = goto l by B7;
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) <> halt SCM+FSA by X, TX;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,mm))) <> halt SCM+FSA ; :: thesis: verum