let k be Nat; :: thesis: for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N; :: thesis: for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let INS be Instruction of S; :: thesis: for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let s be State of S; :: thesis: Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

thus Exec ((IncAddr (INS,k)),(IncIC (s,k))) = Exec ((IncAddr (INS,(0 + k))),(IncIC (s,k)))

.= IncIC ((Exec ((IncAddr (INS,0)),s)),k) by Def1

.= IncIC ((Exec (INS,s)),k) by COMPOS_0:3 ; :: thesis: verum

for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N; :: thesis: for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let INS be Instruction of S; :: thesis: for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

let s be State of S; :: thesis: Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

thus Exec ((IncAddr (INS,k)),(IncIC (s,k))) = Exec ((IncAddr (INS,(0 + k))),(IncIC (s,k)))

.= IncIC ((Exec ((IncAddr (INS,0)),s)),k) by Def1

.= IncIC ((Exec (INS,s)),k) by COMPOS_0:3 ; :: thesis: verum