let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for J being Program of SCM+FSA st NPP s1 = NPP s2 & J is_halting_on Initialized s1,P holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
let s1, s2 be State of SCM+FSA; :: thesis: for J being Program of SCM+FSA st NPP s1 = NPP s2 & J is_halting_on Initialized s1,P holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
let J be Program of SCM+FSA; :: thesis: ( NPP s1 = NPP s2 & J is_halting_on Initialized s1,P implies NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2)) )
assume NPP s1 = NPP s2 ; :: thesis: ( not J is_halting_on Initialized s1,P or NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2)) )
then A: NPP (s1 +* (Initialize ((intloc 0) .--> 1))) = (NPP s2) +* (NPP (Initialize ((intloc 0) .--> 1))) by COMPOS_1:221
.= NPP (s2 +* (Initialize ((intloc 0) .--> 1))) by COMPOS_1:221 ;
D: Initialize ((intloc 0) .--> 1) c= s1 +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
assume J is_halting_on Initialized s1,P ; :: thesis: NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
then P +* J halts_on Initialize (Initialized s1) by SCMFSA7B:def 8;
then B: P +* J halts_on Initialized s1 by SCMFSA6A:83;
thus NPP (IExec (J,P,s1)) = NPP ((Result ((P +* J),(s1 +* (Initialize ((intloc 0) .--> 1))))) +* (s1 | NAT)) by SCMFSA6B:def 1
.= (NPP (Result ((P +* J),(s1 +* (Initialize ((intloc 0) .--> 1)))))) +* (NPP (s1 | NAT)) by COMPOS_1:221
.= (NPP (Result ((P +* J),(s1 +* (Initialize ((intloc 0) .--> 1)))))) +* {}
.= NPP (Result ((P +* J),(s1 +* (Initialize ((intloc 0) .--> 1))))) by FUNCT_4:22
.= NPP (Result ((P +* J),(s2 +* (Initialize ((intloc 0) .--> 1))))) by A, B, AMISTD_2:71
.= (NPP (Result ((P +* J),(s2 +* (Initialize ((intloc 0) .--> 1)))))) +* {} by FUNCT_4:22
.= (NPP (Result ((P +* J),(s2 +* (Initialize ((intloc 0) .--> 1)))))) +* (NPP (s2 | NAT))
.= NPP ((Result ((P +* J),(s2 +* (Initialize ((intloc 0) .--> 1))))) +* (s2 | NAT)) by COMPOS_1:221
.= NPP (IExec (J,P,s2)) by SCMFSA6B:def 1 ; :: thesis: verum