let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location holds NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (IExec (I,P,s))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being Int-Location holds NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (IExec (I,P,s))
let I be Program of SCM+FSA; :: thesis: for a being Int-Location holds NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (IExec (I,P,s))
let a be Int-Location ; :: thesis: NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (IExec (I,P,s))
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* I;
A1: IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = IC (IExec (I,P,s)) by SCMFSA8A:7;
A2: DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (IExec (I,P,s)) by Th35;
then A3: for f being FinSeq-Location holds (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f = (IExec (I,P,s)) . f by SCMFSA6A:38;
for a being Int-Location holds (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . a = (IExec (I,P,s)) . a by A2, SCMFSA6A:38;
hence NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (IExec (I,P,s)) by A3, A1, SCMFSA10:91; :: thesis: verum