let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting relocable AMI-Struct of N
for INS being Instruction of S
for s being State of S
for j, k being Element of NAT st IC s = j + k holds
NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting relocable AMI-Struct of N; :: thesis: for INS being Instruction of S
for s being State of S
for j, k being Element of NAT st IC s = j + k holds
NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k))
let INS be Instruction of S; :: thesis: for s being State of S
for j, k being Element of NAT st IC s = j + k holds
NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k))
let s be State of S; :: thesis: for j, k being Element of NAT st IC s = j + k holds
NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k))
let j, k be Element of NAT ; :: thesis: ( IC s = j + k implies NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k)) )
assume A1: IC s = j + k ; :: thesis: NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k))
set s1 = s +* (Start-At (j,S));
IncIC ((s +* (Start-At (j,S))),k) = s +* (Start-At ((IC s),S)) by A1, COMPOS_1:163
.= s by COMPOS_1:165 ;
then A3: NPP (Exec ((IncAddr (INS,k)),s)) = NPP (IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)) by Th4;
thus NPP (Exec (INS,(DecIC (s,k)))) = NPP (Exec (INS,(s +* (Start-At (j,S))))) by A1, NAT_D:34
.= NPP ((Exec (INS,(s +* (Start-At (j,S))))) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S))) by COMPOS_1:165
.= NPP ((IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S))) by FUNCT_4:122
.= NPP (DecIC ((IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)),k)) by COMPOS_1:166
.= DecIC ((NPP (IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k))),k) by COMPOS_1:229
.= DecIC ((NPP (Exec ((IncAddr (INS,k)),s))),k) by A3
.= NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k)) by COMPOS_1:229 ; :: thesis: verum