let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for p being NAT -defined the InstructionsF of b_{1} -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; :: thesis: 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; :: thesis: 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; :: thesis: for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))

let k be Nat; :: thesis: Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))

deffunc H_{1}( 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) = H_{1}(i,f . i)
by A3;

A8: for i being Nat holds g . (i + 1) = H_{1}(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; :: thesis: verum

for p being NAT -defined the InstructionsF of b

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; :: thesis: 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; :: thesis: 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; :: thesis: for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))

let k be Nat; :: thesis: Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))

deffunc H

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) = H

A8: for i being Nat holds g . (i + 1) = H

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; :: thesis: verum