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
NPP (Result (P,s1)) = NPP (Result (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 st P halts_on s1 holds
NPP (Result (P,s1)) = NPP (Result (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 st P halts_on s1 holds
NPP (Result (P,s1)) = NPP (Result (P,s2)) )
assume Z1: NPP s1 = NPP s2 ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT st P halts_on s1 holds
NPP (Result (P,s1)) = NPP (Result (P,s2))
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( P halts_on s1 implies NPP (Result (P,s1)) = NPP (Result (P,s2)) )
assume Z2: P halts_on s1 ; :: thesis: NPP (Result (P,s1)) = NPP (Result (P,s2))
consider k1 being Nat such that
IC (Comput (P,s1,k1)) in dom P and
W2: CurInstr (P,(Comput (P,s1,k1))) = halt S by Z2, EXTPRO_1:def 7;
C: P halts_on s2 by Z1, Z2, Th69;
then consider k2 being Nat such that
IC (Comput (P,s2,k2)) in dom P and
W4: CurInstr (P,(Comput (P,s2,k2))) = halt S by EXTPRO_1:def 7;
reconsider k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def 13;
reconsider k = max (k1,k2) as Element of NAT by ORDINAL1:def 13;
k1 <= k by XXREAL_0:25;
then D: Comput (P,s1,k) = Comput (P,s1,k1) by W2, EXTPRO_1:6;
k2 <= k by XXREAL_0:25;
then E: Comput (P,s2,k2) = Comput (P,s2,k) by W4, EXTPRO_1:6;
A: Result (P,s1) = Comput (P,s1,k) by Z2, W2, EXTPRO_1:def 8, D;
F: Result (P,s2) = Comput (P,s2,k) by C, W4, EXTPRO_1:def 8, E;
NPP (Comput (P,s1,k)) = NPP (Comput (P,s2,k)) by Z1, ThY;
hence NPP (Result (P,s1)) = NPP (Result (P,s2)) by A, F; :: thesis: verum