let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for e being Nat
for I being Instruction of S
for t being b₂ -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for e being Nat
for I being Instruction of S
for t being b₁ -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let e be Nat; :: thesis: for I being Instruction of S
for t being e -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let I be Instruction of S; :: thesis: for t being e -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let t be e -started State of S; :: thesis: for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let u be Instruction-Sequence of S; :: thesis: ( e .--> I c= u implies Following (u,t) = Exec (I,t) )
assume A1: e .--> I c= u ; :: thesis: Following (u,t) = Exec (I,t)
A2: e in dom (e .--> I) by TARSKI:def 1;
IC t = e by MEMSTR_0:def 11;
then CurInstr (u,t) = u . e by PBOOLE:143
.= (e .--> I) . e by A1, A2, GRFUNC_1:2
.= I by FUNCOP_1:72 ;
hence Following (u,t) = Exec (I,t) ; :: thesis: verum