let k be natural number ; for R being good Ring
for s1, s2, s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated p,k c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) )
let R be good Ring; for s1, s2, s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated p,k c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) )
let s1, s2, s be State of (SCM R); ( not R is trivial implies for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated p,k c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
assume A1:
not R is trivial
; for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated p,k c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) )
let p be autonomic FinPartState of (SCM R); ( IC (SCM R) in dom p & p c= s1 & Relocated p,k c= s2 & s = s1 +* (DataPart s2) implies for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
assume that
A2:
IC (SCM R) in dom p
and
A3:
p c= s1
and
A4:
Relocated p,k c= s2
and
A5:
s = s1 +* (DataPart s2)
; for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) )
defpred S1[ Element of NAT ] means ( (IC (Comput (ProgramPart s1),s1,$1)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,$1) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,$1)),(Comput (ProgramPart s1),s1,$1)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,$1)),(Comput (ProgramPart s2),s2,$1) & (Comput (ProgramPart s1),s1,$1) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,$1) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,$1) = DataPart (Comput (ProgramPart s2),s2,$1) );
A6:
not p is NAT -defined
by A2, AMI_1:109;
A7:
IC p = IC s1
by A2, A3, GRFUNC_1:8;
then
IC p = IC (Comput (ProgramPart s1),s1,0 )
by AMI_1:13;
then A8:
IC p in dom (ProgramPart p)
by A1, A3, A6, Th27;
A9:
p c= s
by A3, A4, A5, Th34;
A10:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set DPp =
DataPart p;
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume that A11:
(IC (Comput (ProgramPart s1),s1,i)) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,i)
and A12:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i)
and A13:
(Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k)))
and A14:
DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i)
;
S1[i + 1]
set Cs2i1 =
Comput (ProgramPart s2),
s2,
(i + 1);
set Cs3i =
Comput (ProgramPart s),
s,
i;
set Cs2i =
Comput (ProgramPart s2),
s2,
i;
T:
ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,i)
by AMI_1:144;
A15:
Comput (ProgramPart s2),
s2,
(i + 1) =
Following (ProgramPart s2),
(Comput (ProgramPart s2),s2,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i)
by T
;
A17:
now let d be
Data-Location of
R;
(Comput (ProgramPart s),s,i) . d = (Comput (ProgramPart s2),s2,i) . dA18:
d in dom (DataPart (Comput (ProgramPart s),s,i))
by A16;
hence (Comput (ProgramPart s),s,i) . d =
(DataPart (Comput (ProgramPart s),s,i)) . d
by FUNCT_1:70
.=
(Comput (ProgramPart s2),s2,i) . d
by A14, A18, FUNCT_1:70
;
verum end;
set Cs1i1 =
Comput (ProgramPart s1),
s1,
(i + 1);
set Cs1i =
Comput (ProgramPart s1),
s1,
i;
dom (Comput (ProgramPart s1),s1,(i + 1)) = the
carrier of
(SCM R)
by PARTFUN1:def 4;
then A19:
dom (Comput (ProgramPart s1),s1,(i + 1)) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT
by Th1;
consider j being
natural number such that A20:
IC (Comput (ProgramPart s1),s1,i) = il. (SCM R),
j
by AMISTD_1:26;
A21:
succ ((IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R)) =
succ (il. (SCM R),(j + k))
by A20, AMISTD_1:def 13
.=
il. (SCM R),
((j + k) + 1)
by SCMRING3:67
.=
il. (SCM R),
((j + 1) + k)
.=
(il. (SCM R),(j + 1)) + k,
(SCM R)
by AMISTD_1:def 13
.=
(succ (IC (Comput (ProgramPart s1),s1,i))) + k,
(SCM R)
by A20, SCMRING3:67
;
A22:
now reconsider loc =
IC (Comput (ProgramPart s1),s1,(i + 1)) as
Element of
NAT ;
assume A23:
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
;
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1))A24:
loc in dom (ProgramPart p)
by A1, A3, A6, Th27;
ProgramPart p c= p
by RELAT_1:88;
then A25:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then
loc + k,
(SCM R) in dom (Relocated p,k)
by A24, AMISTD_2:71;
then A26:
(Relocated p,k) . (loc + k,(SCM R)) =
s2 . (loc + k,(SCM R))
by A4, GRFUNC_1:8
.=
(Comput (ProgramPart s2),s2,(i + 1)) . (loc + k,(SCM R))
by AMI_1:54
;
Y:
(ProgramPart (Comput (ProgramPart s1),s1,(i + 1))) /. loc = (Comput (ProgramPart s1),s1,(i + 1)) . loc
by AMI_1:150;
Z:
(ProgramPart (Comput (ProgramPart s2),s2,(i + 1))) /. (IC (Comput (ProgramPart s2),s2,(i + 1))) = (Comput (ProgramPart s2),s2,(i + 1)) . (IC (Comput (ProgramPart s2),s2,(i + 1)))
by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),
(Comput (ProgramPart s1),s1,(i + 1)) =
s1 . loc
by AMI_1:54, Y
.=
p . loc
by A3, A24, A25, GRFUNC_1:8
;
hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A23, A24, A26, AMISTD_2:76, Z;
verum end;
dom (Comput (ProgramPart s2),s2,i) = the
carrier of
(SCM R)
by PARTFUN1:def 4;
then A27:
dom (Comput (ProgramPart s2),s2,i) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT
by Th1;
Data-Locations (SCM R) = SCM-Data-Loc
by SCMRING2:31;
then
dom (DataPart p) = (dom p) /\ SCM-Data-Loc
by RELAT_1:90;
then A28:
dom (DataPart p) c= {(IC (SCM R))} \/ SCM-Data-Loc
by XBOOLE_1:10, XBOOLE_1:17;
set Cs3i1 =
Comput (ProgramPart s),
s,
(i + 1);
A29:
dom (DataPart (Comput (ProgramPart s2),s2,i)) = SCM-Data-Loc
by Th9;
A30:
dom (DataPart (Comput (ProgramPart s),s,(i + 1))) = SCM-Data-Loc
by Th9;
then A31:
dom (DataPart (Comput (ProgramPart s),s,(i + 1))) c= dom (DataPart (Comput (ProgramPart s2),s2,(i + 1)))
by Th9;
A32:
dom (DataPart (Comput (ProgramPart s2),s2,(i + 1))) = SCM-Data-Loc
by Th9;
A33:
now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) & (Comput (ProgramPart s),s,(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume that A34:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
and A35:
(Comput (ProgramPart s),s,(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthus (DataPart (Comput (ProgramPart s),s,(i + 1))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . x
by A34, A35, FUNCT_1:70
.=
(DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A30, A32, A34, FUNCT_1:70
;
verum end;
A36:
dom (DataPart (Comput (ProgramPart s),s,i)) = SCM-Data-Loc
by Th9;
A37:
now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) & (Comput (ProgramPart s),s,(i + 1)) . x = (Comput (ProgramPart s),s,i) . x & (Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume that A38:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
and A39:
(
(Comput (ProgramPart s),s,(i + 1)) . x = (Comput (ProgramPart s),s,i) . x &
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x )
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
(DataPart (Comput (ProgramPart s),s,i)) . x = (Comput (ProgramPart s),s,i) . x
by A36, A30, A38, FUNCT_1:70;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A29, A30, A33, A38, A39, FUNCT_1:70;
verum end;
dom (Comput (ProgramPart s1),s1,i) = the
carrier of
(SCM R)
by PARTFUN1:def 4;
then A40:
dom (Comput (ProgramPart s1),s1,i) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT
by Th1;
dom (Comput (ProgramPart s2),s2,(i + 1)) = the
carrier of
(SCM R)
by PARTFUN1:def 4;
then A41:
dom (Comput (ProgramPart s2),s2,(i + 1)) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT
by Th1;
set I =
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i);
T:
ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,i)
by AMI_1:144;
A42:
Comput (ProgramPart s1),
s1,
(i + 1) =
Following (ProgramPart s1),
(Comput (ProgramPart s1),s1,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i)
by T
;
A43:
dom ((Comput (ProgramPart s1),s1,i) | (dom (DataPart p))) =
(dom (Comput (ProgramPart s1),s1,i)) /\ (dom (DataPart p))
by RELAT_1:90
.=
dom (DataPart p)
by A40, A28, XBOOLE_1:10, XBOOLE_1:28
;
A44:
dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) =
(dom (Comput (ProgramPart s1),s1,(i + 1))) /\ (dom (DataPart p))
by RELAT_1:90
.=
dom (DataPart p)
by A19, A28, XBOOLE_1:10, XBOOLE_1:28
;
A45:
dom (DataPart p) = dom (DataPart (Relocated p,k))
by AMISTD_2:68;
then A46:
dom ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))) =
(dom (Comput (ProgramPart s2),s2,(i + 1))) /\ (dom (DataPart p))
by RELAT_1:90
.=
dom (DataPart p)
by A41, A28, XBOOLE_1:10, XBOOLE_1:28
;
then A47:
dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) c= dom ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p)))
by A44, AMISTD_2:68;
A48:
dom ((Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k)))) =
(dom (Comput (ProgramPart s2),s2,i)) /\ (dom (DataPart p))
by A45, RELAT_1:90
.=
dom (DataPart p)
by A27, A28, XBOOLE_1:10, XBOOLE_1:28
;
A49:
now let x be
set ;
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d & (Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d holds
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . xlet d be
Data-Location of
R;
( d = x & d in dom (DataPart p) & (Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d & (Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume that A50:
d = x
and A51:
d in dom (DataPart p)
and A52:
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . xA53:
(
((Comput (ProgramPart s1),s1,i) | (dom (DataPart p))) . d = (Comput (ProgramPart s1),s1,i) . d &
((Comput (ProgramPart s2),s2,i) | (dom (DataPart p))) . d = (Comput (ProgramPart s2),s2,i) . d )
by A45, A43, A48, A51, FUNCT_1:70;
thus ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s1),s1,(i + 1)) . d
by A44, A50, A51, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A13, A45, A46, A50, A51, A52, A53, FUNCT_1:70
;
verum end;
A54:
now let x be
set ;
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s2),s2,(i + 1)) . d holds
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . xlet d be
Data-Location of
R;
( d = x & d in dom (DataPart p) & (Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s2),s2,(i + 1)) . d implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume that A55:
(
d = x &
d in dom (DataPart p) )
and A56:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s2),s2,(i + 1)) . d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . xthus ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . d
by A44, A55, A56, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A45, A46, A55, FUNCT_1:70
;
verum end;
T:
ProgramPart s = ProgramPart (Comput (ProgramPart s),s,i)
by AMI_1:144;
A57:
Comput (ProgramPart s),
s,
(i + 1) =
Following (ProgramPart s),
(Comput (ProgramPart s),s,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s),s,i)
by A1, A3, A6, A9, Th28, T
;
per cases
( InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 0 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 1 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 2 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 3 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 4 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 5 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 6 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 7 )
by NAT_1:32, SCMRING3:71;
suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 0
;
S1[i + 1]then A58:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = halt (SCM R)
by SCMRING3:16;
hence (IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) =
(IC (Comput (ProgramPart s1),s1,i)) + k,
(SCM R)
by A42, AMI_1:def 8
.=
IC (Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A15, A58, AMI_1:def 8
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A22;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A59:
Comput (ProgramPart s2),
s2,
(i + 1) = Comput (ProgramPart s2),
s2,
i
by A12, A15, A58, AMI_1:def 8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A13, A42, A58, AMI_1:def 8;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))thus
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A14, A57, A58, A59, AMI_1:def 8;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 1
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A60:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da := db
by SCMRING3:17;
A61:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = da := db
by A60, AMISTD_2:29;
A62:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC (SCM R)) = succ (IC (Comput (ProgramPart s1),s1,i))
by A60, SCMRING2:13;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A42, A15, A21, A61, SCMRING2:13;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A22, A42, A15, A21, A61, A62, SCMRING2:13;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A63:
(Comput (ProgramPart s),s,i) . db = (Comput (ProgramPart s2),s2,i) . db
by A17;
now
DataPart p c= p
by RELAT_1:88;
then A64:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A65:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A65, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose A66:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . db &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . db )
by A12, A42, A15, A60, A61, SCMRING2:13;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A1, A3, A6, A9, A44, A54, A60, A63, A65, A64, A66, Th29;
verum end; suppose
da <> d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A42, A15, A60, A61, SCMRING2:13;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A65;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A67:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . db &
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . db )
by A12, A15, A57, A60, A61, SCMRING2:13;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A17, A33, A67;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A15, A57, A60, A61, SCMRING2:13;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A67;
verum end; end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 2
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A68:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = AddTo da,
db
by SCMRING3:18;
A69:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = AddTo da,
db
by A68, AMISTD_2:29;
A70:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC (SCM R)) = succ (IC (Comput (ProgramPart s1),s1,i))
by A68, SCMRING2:14;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A42, A15, A21, A69, SCMRING2:14;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A22, A42, A15, A21, A69, A70, SCMRING2:14;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A71:
(
(Comput (ProgramPart s),s,i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s),s,i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A17;
now
DataPart p c= p
by RELAT_1:88;
then A72:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A73:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A73, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose A74:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = ((Comput (ProgramPart s1),s1,i) . da) + ((Comput (ProgramPart s1),s1,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) + ((Comput (ProgramPart s2),s2,i) . db) )
by A12, A42, A15, A68, A69, SCMRING2:14;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A1, A3, A6, A9, A44, A54, A68, A71, A73, A72, A74, Th30;
verum end; suppose
da <> d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A42, A15, A68, A69, SCMRING2:14;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A73;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A75:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) + ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s),s,(i + 1)) . d = ((Comput (ProgramPart s),s,i) . da) + ((Comput (ProgramPart s),s,i) . db) )
by A12, A15, A57, A68, A69, SCMRING2:14;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A33, A71, A75;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A15, A57, A68, A69, SCMRING2:14;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A75;
verum end; end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 3
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A76:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = SubFrom da,
db
by SCMRING3:19;
A77:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = SubFrom da,
db
by A76, AMISTD_2:29;
A78:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC (SCM R)) = succ (IC (Comput (ProgramPart s1),s1,i))
by A76, SCMRING2:15;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A42, A15, A21, A77, SCMRING2:15;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A22, A42, A15, A21, A77, A78, SCMRING2:15;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A79:
(
(Comput (ProgramPart s),s,i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s),s,i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A17;
now
DataPart p c= p
by RELAT_1:88;
then A80:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A81:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A81, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose A82:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = ((Comput (ProgramPart s1),s1,i) . da) - ((Comput (ProgramPart s1),s1,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) - ((Comput (ProgramPart s2),s2,i) . db) )
by A12, A42, A15, A76, A77, SCMRING2:15;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A1, A3, A6, A9, A44, A54, A76, A79, A81, A80, A82, Th31;
verum end; suppose
da <> d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A42, A15, A76, A77, SCMRING2:15;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A81;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A83:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) - ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s),s,(i + 1)) . d = ((Comput (ProgramPart s),s,i) . da) - ((Comput (ProgramPart s),s,i) . db) )
by A12, A15, A57, A76, A77, SCMRING2:15;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A33, A79, A83;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A15, A57, A76, A77, SCMRING2:15;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A83;
verum end; end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 4
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A84:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = MultBy da,
db
by SCMRING3:20;
A85:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = MultBy da,
db
by A84, AMISTD_2:29;
A86:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC (SCM R)) = succ (IC (Comput (ProgramPart s1),s1,i))
by A84, SCMRING2:16;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A42, A15, A21, A85, SCMRING2:16;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A22, A42, A15, A21, A85, A86, SCMRING2:16;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A87:
(
(Comput (ProgramPart s),s,i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s),s,i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A17;
now
DataPart p c= p
by RELAT_1:88;
then A88:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A89:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A89, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose A90:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = ((Comput (ProgramPart s1),s1,i) . da) * ((Comput (ProgramPart s1),s1,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) * ((Comput (ProgramPart s2),s2,i) . db) )
by A12, A42, A15, A84, A85, SCMRING2:16;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A1, A3, A6, A9, A44, A54, A84, A87, A89, A88, A90, Th32;
verum end; suppose
da <> d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A42, A15, A84, A85, SCMRING2:16;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A89;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A91:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) * ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s),s,(i + 1)) . d = ((Comput (ProgramPart s),s,i) . da) * ((Comput (ProgramPart s),s,i) . db) )
by A12, A15, A57, A84, A85, SCMRING2:16;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A33, A87, A91;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A15, A57, A84, A85, SCMRING2:16;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A91;
verum end; end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 5
;
S1[i + 1]then consider da being
Data-Location of
R,
r being
Element of
R such that A92:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da := r
by SCMRING3:21;
A93:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = da := r
by A92, AMISTD_2:29;
A94:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC (SCM R)) = succ (IC (Comput (ProgramPart s1),s1,i))
by A92, SCMRING2:19;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A42, A15, A21, A93, SCMRING2:19;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A11, A12, A22, A42, A15, A21, A93, A94, SCMRING2:19;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A95:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A95, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose A96:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1thus ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s1),s1,(i + 1)) . d
by A44, A95, FUNCT_1:72
.=
r
by A42, A92, A96, SCMRING2:19
.=
(Comput (ProgramPart s2),s2,(i + 1)) . d
by A12, A15, A93, A96, SCMRING2:19
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A95, FUNCT_1:72
;
verum end; suppose
da <> d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A42, A15, A92, A93, SCMRING2:19;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A95;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A97:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = r &
(Comput (ProgramPart s),s,(i + 1)) . d = r )
by A12, A15, A57, A92, A93, SCMRING2:19;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A33, A97;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A12, A15, A57, A92, A93, SCMRING2:19;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A97;
verum end; end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 6
;
S1[i + 1]then consider loc being
Element of
NAT such that A98:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = goto loc,
R
by SCMRING3:22;
A99:
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) = goto (loc + k,(SCM R)),
R
by A12, A98, SCMRING3:69;
thus (IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) =
loc + k,
(SCM R)
by A42, A98, SCMRING2:17
.=
IC (Comput (ProgramPart s2),s2,(i + 1))
by A15, A99, SCMRING2:17
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A22;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume A100:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A100, SCMRING2:1;
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A42, A15, A98, A99, SCMRING2:17;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A100;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A101:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A15, A57, A98, A99, SCMRING2:17;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A101;
verum end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 7
;
S1[i + 1]then consider da being
Data-Location of
R,
loc being
Element of
NAT such that A102:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da =0_goto loc
by SCMRING3:23;
A104:
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) = da =0_goto (loc + k,(SCM R))
by A12, A102, SCMRING3:70;
A106:
(Comput (ProgramPart s),s,i) . da = (Comput (ProgramPart s2),s2,i) . da
by A17;
now per cases
( loc <> succ (IC (Comput (ProgramPart s1),s1,i)) or loc = succ (IC (Comput (ProgramPart s1),s1,i)) )
;
suppose
loc <> succ (IC (Comput (ProgramPart s1),s1,i))
;
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1))
by A1, A3, A6, A9, A102, A106, A103, A105, Th33;
verum end; hence
(
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,(i + 1)) &
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1)) )
by A22;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume A107:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
dom (DataPart p) c= SCM-Data-Loc
by Th13;
then reconsider d =
x as
Data-Location of
R by A44, A107, SCMRING2:1;
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A42, A15, A102, A104, SCMRING2:18;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A49, A107;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A47, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A45, A44, A46, GRFUNC_1:9;
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s),s,(i + 1))) implies (DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A108:
x in dom (DataPart (Comput (ProgramPart s),s,(i + 1)))
;
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen reconsider d =
x as
Data-Location of
R by A30, SCMRING2:1;
(
(Comput (ProgramPart s),s,(i + 1)) . d = (Comput (ProgramPart s),s,i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A15, A57, A102, A104, SCMRING2:18;
hence
(DataPart (Comput (ProgramPart s),s,(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A37, A108;
verum end; then
DataPart (Comput (ProgramPart s),s,(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A31, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s),s,(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A30, A32, GRFUNC_1:9;
verum end;
end;
Y:
(ProgramPart s1) /. (IC s1) = s1 . (IC s1)
by AMI_1:150;
Comput (ProgramPart s1),s1,0 = s1
by AMI_1:13;
then A109: IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,0 )),(Comput (ProgramPart s1),s1,0 )),k =
IncAddr (CurInstr (ProgramPart s1),s1),k
.=
IncAddr (s1 . (IC s1)),k
by Y
;
A110:
DataPart (Relocated p,k) c= Relocated p,k
by RELAT_1:88;
A111:
DataPart p c= p
by RELAT_1:88;
A112:
DataPart p = DataPart (Relocated p,k)
by AMISTD_2:68;
A113: (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
by AMI_1:13
.=
DataPart p
by A3, A111, GRFUNC_1:64, XBOOLE_1:1
.=
s2 | (dom (DataPart p))
by A4, A112, A110, GRFUNC_1:64, XBOOLE_1:1
.=
(Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k)))
by A112, AMI_1:13
;
A114: DataPart (Comput (ProgramPart s),s,0 ) =
DataPart (s1 +* (DataPart s2))
by A5, AMI_1:13
.=
DataPart s2
by PBOOLE:157
.=
DataPart (Comput (ProgramPart s2),s2,0 )
by AMI_1:13
;
A115:
IC (SCM R) in dom (Relocated p,k)
by AMISTD_2:72;
A116: (IC (Comput (ProgramPart s1),s1,0 )) + k,(SCM R) =
(IC s1) + k,(SCM R)
by AMI_1:13
.=
(IC p) + k,(SCM R)
by A2, A3, GRFUNC_1:8
.=
IC (Relocated p,k)
by AMISTD_2:73
.=
IC s2
by A4, A115, GRFUNC_1:8
.=
IC (Comput (ProgramPart s2),s2,0 )
by AMI_1:13
;
A117:
IC (SCM R) in dom (Relocated p,k)
by AMISTD_2:72;
ProgramPart p c= p
by RELAT_1:88;
then A118:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then A119:
(IC p) + k,(SCM R) in dom (Relocated p,k)
by A8, AMISTD_2:71;
Y:
(ProgramPart s2) /. (IC (Relocated p,k)) = s2 . (IC (Relocated p,k))
by AMI_1:150;
Comput (ProgramPart s2),s2,0 = s2
by AMI_1:13;
then A120: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,0 )),(Comput (ProgramPart s2),s2,0 ) =
CurInstr (ProgramPart s2),s2
.=
s2 . (IC (Relocated p,k))
by A4, A117, GRFUNC_1:8, Y
.=
s2 . ((IC p) + k,(SCM R))
by AMISTD_2:73
.=
(Relocated p,k) . ((IC p) + k,(SCM R))
by A4, A119, GRFUNC_1:8
;
p . (IC p) = s1 . (IC s1)
by A3, A7, A8, A118, GRFUNC_1:8;
then A121:
S1[ 0 ]
by A116, A8, A109, A120, A113, A114, AMISTD_2:76;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A121, A10);
hence
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k,(SCM R) = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) )
; verum