let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting relocable AMI-Struct of 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 non empty with_non-empty_elements set ; :: thesis: for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting relocable AMI-Struct of 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 standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting relocable AMI-Struct of 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_1:10 ; :: thesis: verum