let l be Instruction-Location of SCM+FSA ; :: thesis: for s being State of SCM+FSA st IC s = l & s . l = goto l holds
not s is halting
let s be State of SCM+FSA ; :: thesis: ( IC s = l & s . l = goto l implies not s is halting )
set S = s;
assume that
A1: IC s = l and
A2: s . l = goto l ; :: thesis: not s is halting
A3: CurInstr s = goto l by A1, A2;
defpred S₁[ Element of NAT ] means Computation s,$1 = s;
A4: S₁[ 0 ] by AMI_1:13;
A5: 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] )
A6: IC (Exec (goto l),s) = IC s by A1, SCMFSA_2:95;
A7: for a being Int-Location holds (Exec (goto l),s) . a = s . a by SCMFSA_2:95;
A8: for f being FinSeq-Location holds (Exec (goto l),s) . f = s . f by SCMFSA_2:95;
A9: for i being Instruction-Location of SCM+FSA holds (Exec (goto l),s) . i = s . i by AMI_1:def 13;
assume Computation s,m = s ; :: thesis: S₁[m + 1]
hence Computation s,(m + 1) = Following s by AMI_1:14
.= s by A1, A2, A6, A7, A8, A9, SCMFSA_2:86 ;
:: thesis: verum

end;

A10: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A4, A5);
let m be Element of NAT ; :: according to AMI_1:def 20 :: thesis: not CurInstr (Computation s,m) = halt SCM+FSA
CurInstr (Computation s,m) = goto l by A3, A10;
hence not CurInstr (Computation s,m) = halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124; :: thesis: verum