let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for J being parahalting Program of SCM+FSA st NPP s1 = NPP s2 holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
let s1, s2 be State of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA st NPP s1 = NPP s2 holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
let J be parahalting Program of SCM+FSA; :: thesis: ( NPP s1 = NPP s2 implies NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2)) )
assume NPP s1 = NPP s2 ; :: thesis: 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;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then C: Start-At (0,SCM+FSA) c= s1 +* (Initialize ((intloc 0) .--> 1)) by D, XBOOLE_1:1;
J c= P +* J by FUNCT_4:26;
then B: P +* J halts_on s1 +* (Initialize ((intloc 0) .--> 1)) by C, SCMFSA6B:def 3;
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