let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for s being State of S
for k being Nat holds Computation s,(k + 1) = Following (Computation s,k)
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for s being State of S
for k being Nat holds Computation s,(k + 1) = Following (Computation s,k)
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis: for s being State of S
for k being Nat holds Computation s,(k + 1) = Following (Computation s,k)
let s be State of S; :: thesis: for k being Nat holds Computation s,(k + 1) = Following (Computation s,k)
let k be Nat; :: thesis: Computation s,(k + 1) = Following (Computation s,k)
deffunc H₁( set , State of S) -> State of S = Following $2;
consider f being Function of NAT , product the Object-Kind of S such that
W1: Computation s,(k + 1) = f . (k + 1) and
W2: f . 0 = s and
W3: for i being Nat holds f . (i + 1) = H₁(i,f . i) by Def19;
consider g being Function of NAT , product the Object-Kind of S such that
V1: Computation s,k = g . k and
V2: g . 0 = s and
V3: for i being Nat holds g . (i + 1) = H₁(i,g . i) by Def19;
f = g from NAT_1:sch 16(W2, W3, V2, V3);
hence Computation s,(k + 1) = Following (Computation s,k) by V1, V3, W1; :: thesis: verum