let l be Element of NAT ; :: thesis: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st IC s = l & P . l = goto l holds
not P halts_on s
let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st IC s = l & P . l = goto l holds
not P halts_on s
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( IC s = l & P . l = goto l implies not P halts_on s )
assume that
A1: IC s = l and
A2: P . l = goto l ; :: thesis: not P halts_on s
A6: P /. (IC s) = P . (IC s) by PBOOLE:158;
defpred S₁[ Nat] means NPP (Comput (P,s,$1)) = NPP 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 by 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;
assume Z: NPP (Comput (P,s,m)) = NPP s ; :: thesis: S₁[m + 1]
hence NPP (Comput (P,s,(m + 1))) = NPP (Following (P,(Comput (P,s,m)))) by EXTPRO_1:4
.= NPP (Following (P,s)) by Z, AMISTD_2:67
.= NPP s by A1, A2, A5, A4, A6, SCMFSA_2:138 ;
:: thesis: verum

end;

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