let k be Element of NAT ; :: thesis: for s being State of holds Computation s,(k + 1) = Exec (CurInstr (Computation s,k)),(Computation s,k)
let s be State of ; :: thesis: Computation s,(k + 1) = Exec (CurInstr (Computation s,k)),(Computation s,k)
thus Computation s,(k + 1) = Following (Computation s,k) by AMI_1:14
.= Exec (CurInstr (Computation s,k)),(Computation s,k) ; :: thesis: verum