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_{2} -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_{1} -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

for e being Nat

for I being Instruction of S

for t being b

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

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