let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -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 IC-Ins-separated AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions 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 Instructions 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₁( set , State of S) -> Element of product the Object-Kind of S = down (Following (p,$2));
reconsider s = s as Element of product the Object-Kind of S by CARD_3:107;
consider f being Function of NAT,(product the Object-Kind 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 Def6;
consider g being Function of NAT,(product the Object-Kind 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 Def6;
A7: for i being Nat holds f . (i + 1) = H₁(i,f . i) by A3;
A8: for i being Nat holds g . (i + 1) = H₁(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