let N be non empty with_non-empty_elements set ; :: thesis: for k being Element of NAT
for S being non empty IC-Ins-separated AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued finite Function
for s being State of holds Comput p,s,(k + 1) = Exec (p /. (IC (Comput p,s,k))),(Comput p,s,k)
let k be Element of NAT ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -valued finite Function
for s being State of holds Comput p,s,(k + 1) = Exec (p /. (IC (Comput p,s,k))),(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 finite Function
for s being State of holds Comput p,s,(k + 1) = Exec (p /. (IC (Comput p,s,k))),(Comput p,s,k)
let p be NAT -defined the Instructions of S -valued finite Function; :: thesis: for s being State of holds Comput p,s,(k + 1) = Exec (p /. (IC (Comput p,s,k))),(Comput p,s,k)
let s be State of ; :: thesis: Comput p,s,(k + 1) = Exec (p /. (IC (Comput p,s,k))),(Comput p,s,k)
thus Comput p,s,(k + 1) = Following p,(Comput p,s,k) by Th5
.= Exec (p /. (IC (Comput p,s,k))),(Comput p,s,k) ; :: thesis: verum