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 st P halts_on s1 holds
P halts_on 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 st P halts_on s1 holds
P halts_on 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 st P halts_on s1 holds
P halts_on s2 )
assume Z: NPP s1 = NPP s2 ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT st P halts_on s1 holds
P halts_on s2
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( P halts_on s1 implies P halts_on s2 )
assume P halts_on s1 ; :: thesis: P halts_on s2
then consider k being Nat such that
IC (Comput (P,s1,k)) in dom P and
W2: CurInstr (P,(Comput (P,s1,k))) = halt S by EXTPRO_1:def 7;
take k ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,s2,k)) in proj1 P & CurInstr (P,(Comput (P,s2,k))) = halt S )
dom P = NAT by PARTFUN1:def 4;
hence IC (Comput (P,s2,k)) in dom P ; :: thesis: CurInstr (P,(Comput (P,s2,k))) = halt S
NPP (Comput (P,s1,k)) = NPP (Comput (P,s2,k)) by Z, ThY;
then IC (Comput (P,s1,k)) = IC (Comput (P,s2,k)) by COMPOS_1:230;
hence CurInstr (P,(Comput (P,s2,k))) = P /. (IC (Comput (P,s1,k)))
.= halt S by W2 ;
:: thesis: verum