let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting Exec-preserving AMI-Struct of N
for s1, s2 being State of S st NPP s1 = NPP s2 holds
for P being the Instructions of b₁ -valued ManySortedSet of NAT holds NPP (Following (P,s1)) = NPP (Following (P,s2))
let S be non empty stored-program IC-Ins-separated definite realistic halting Exec-preserving AMI-Struct of N; :: thesis: for s1, s2 being State of S st NPP s1 = NPP s2 holds
for P being the Instructions of S -valued ManySortedSet of NAT holds NPP (Following (P,s1)) = NPP (Following (P,s2))
let s1, s2 be State of S; :: thesis: ( NPP s1 = NPP s2 implies for P being the Instructions of S -valued ManySortedSet of NAT holds NPP (Following (P,s1)) = NPP (Following (P,s2)) )
assume Z: NPP s1 = NPP s2 ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT holds NPP (Following (P,s1)) = NPP (Following (P,s2))
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: NPP (Following (P,s1)) = NPP (Following (P,s2))
A: CurInstr (P,s1) = CurInstr (P,s2) by Z, COMPOS_1:230;
thus NPP (Following (P,s1)) = NPP (Exec ((CurInstr (P,s1)),s1))
.= NPP (Exec ((CurInstr (P,s2)),s2)) by A, Z, Def20
.= NPP (Following (P,s2)) ; :: thesis: verum