let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s
let loc be Instruction-Location of S; :: thesis: for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s
let l be Element of ObjectKind (IC S); :: thesis: ( l = loc implies for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s )
assume A1: l = loc ; :: thesis: for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s
let h be Element of ObjectKind loc; :: thesis: ( h = halt S implies for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s )
assume A2: h = halt S ; :: thesis: for s being State of S st (IC S),loc --> l,h c= s holds
for i being Element of NAT holds Computation s,i = s
let s be State of S; :: thesis: ( (IC S),loc --> l,h c= s implies for i being Element of NAT holds Computation s,i = s )
assume A3: (IC S),loc --> l,h c= s ; :: thesis: for i being Element of NAT holds Computation s,i = s
defpred S₁[ Element of NAT ] means Computation s,$1 = s;

A4: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
Computation s,(i + 1) = Following (Computation s,i) by Th14
.= Exec (halt S),s by A1, A2, A3, A5, Th64
.= s by Def8 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ] by Th13;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A6, A4); :: thesis: verum