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

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),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

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

let INS be Instruction of S; :: thesis: for s being State of S

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

let s be State of S; :: thesis: for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

let j, k be Nat; :: thesis: ( IC s = j + k implies Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k) )

assume A1: IC s = j + k ; :: thesis: Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

set s1 = s +* (Start-At (j,S));

A2: IncIC ((s +* (Start-At (j,S))),k) = s +* (Start-At ((IC s),S)) by A1, MEMSTR_0:58

.= s by MEMSTR_0:31 ;

thus Exec (INS,(DecIC (s,k))) = Exec (INS,(s +* (Start-At (j,S)))) by A1, NAT_D:34

.= (Exec (INS,(s +* (Start-At (j,S))))) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S)) by MEMSTR_0:31

.= (IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S)) by FUNCT_4:114

.= DecIC ((IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)),k) by MEMSTR_0:59

.= DecIC ((Exec ((IncAddr (INS,k)),s)),k) by A2, Th4 ; :: thesis: verum

for INS being Instruction of S

for s being State of S

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),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

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

let INS be Instruction of S; :: thesis: for s being State of S

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

let s be State of S; :: thesis: for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

let j, k be Nat; :: thesis: ( IC s = j + k implies Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k) )

assume A1: IC s = j + k ; :: thesis: Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

set s1 = s +* (Start-At (j,S));

A2: IncIC ((s +* (Start-At (j,S))),k) = s +* (Start-At ((IC s),S)) by A1, MEMSTR_0:58

.= s by MEMSTR_0:31 ;

thus Exec (INS,(DecIC (s,k))) = Exec (INS,(s +* (Start-At (j,S)))) by A1, NAT_D:34

.= (Exec (INS,(s +* (Start-At (j,S))))) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S)) by MEMSTR_0:31

.= (IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S)) by FUNCT_4:114

.= DecIC ((IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)),k) by MEMSTR_0:59

.= DecIC ((Exec ((IncAddr (INS,k)),s)),k) by A2, Th4 ; :: thesis: verum