let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let p be NAT -defined the InstructionsF of S -valued Function; for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let s be State of S; for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let k be Nat; Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
deffunc H1( set , State of S) -> Element of product (the_Values_of S) = down (Following (p,$2));
reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;
consider f being sequence of (product (the_Values_of S)) such that
A1:
Comput (p,s,(k + 1)) = f . (k + 1)
and
A2:
f . 0 = s
and
A3:
for i being Nat holds f . (i + 1) = Following (p,(f . i))
by Def7;
consider g being sequence of (product (the_Values_of S)) such that
A4:
Comput (p,s,k) = g . k
and
A5:
g . 0 = s
and
A6:
for i being Nat holds g . (i + 1) = Following (p,(g . i))
by Def7;
A7:
for i being Nat holds f . (i + 1) = H1(i,f . i)
by A3;
A8:
for i being Nat holds g . (i + 1) = H1(i,g . i)
by A6;
f = g
from NAT_1:sch 16(A2, A7, A5, A8);
hence
Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
by A1, A4, A6; verum