let k be Element of NAT ; for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
let p be autonomic FinPartState of SCM ; for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
let s1, s2 be State of SCM ; ( IC SCM in dom p & p c= s1 & Relocated p,k c= s2 implies for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
assume that
A1:
IC SCM in dom p
and
A2:
p c= s1
and
A3:
Relocated p,k c= s2
; for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
set s3 = s1 +* (DataPart s2);
TX1:
ProgramPart (s1 +* (DataPart s2)) = ProgramPart s1
by COMPOS_1:39;
defpred S1[ Element of NAT ] means ( (IC (Comput (ProgramPart s1),s1,$1)) + k = IC (Comput (ProgramPart s2),s2,$1) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,$1)),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),$1) = DataPart (Comput (ProgramPart s2),s2,$1) );
A4:
not p is NAT -defined
by A1, COMPOS_1:19;
A5:
p c= s1 +* (DataPart s2)
by A2, A3, Th30;
now set DPp =
DataPart p;
let i be
Element of
NAT ;
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) implies ( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) ) )assume that A6:
(IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i)
and A7:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i)
and A8:
(Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k)))
and A9:
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i)
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )set Cs2i1 =
Comput (ProgramPart s2),
s2,
(i + 1);
T21:
ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(i + 1))
by AMI_1:123;
set Cs3i =
Comput (ProgramPart s1),
(s1 +* (DataPart s2)),
i;
set Cs2i =
Comput (ProgramPart s2),
s2,
i;
A10:
dom (Comput (ProgramPart s2),s2,(i + 1)) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT
by AMI_5:23, PARTFUN1:def 4;
set Cs3i1 =
Comput (ProgramPart s1),
(s1 +* (DataPart s2)),
(i + 1);
A11:
dom (DataPart (Comput (ProgramPart s2),s2,i)) = SCM-Data-Loc
by AMI_3:72, COMPOS_1:50;
A12:
dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) = SCM-Data-Loc
by AMI_3:72, COMPOS_1:50;
A13:
dom (DataPart (Comput (ProgramPart s2),s2,(i + 1))) = SCM-Data-Loc
by AMI_3:72, COMPOS_1:50;
A14:
now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) & (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume that A15:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
and A16:
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthus (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . x
by A15, A16, FUNCT_1:70
.=
(DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A12, A13, A15, FUNCT_1:70
;
verum end; A17:
dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i)) = SCM-Data-Loc
by AMI_3:72, COMPOS_1:50;
A18:
now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) & (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . x & (Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume that A19:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
and A20:
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . x &
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x )
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i)) . x = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . x
by A17, A12, A19, FUNCT_1:70;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A9, A11, A12, A14, A19, A20, FUNCT_1:70;
verum end; A22:
now let d be
Data-Location ;
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d = (Comput (ProgramPart s2),s2,i) . dA23:
d in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i))
by A21;
hence (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d =
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i)) . d
by FUNCT_1:70
.=
(Comput (ProgramPart s2),s2,i) . d
by A9, A23, FUNCT_1:70
;
verum end; set Cs1i1 =
Comput (ProgramPart s1),
s1,
(i + 1);
set Cs1i =
Comput (ProgramPart s1),
s1,
i;
A24:
dom (Comput (ProgramPart s1),s1,(i + 1)) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT
by AMI_5:23, PARTFUN1:def 4;
dom (DataPart p) = (dom p) /\ SCM-Data-Loc
by AMI_3:72, RELAT_1:90;
then A25:
dom (DataPart p) c= {(IC SCM )} \/ SCM-Data-Loc
by XBOOLE_1:10, XBOOLE_1:17;
A26:
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 A24, A25, XBOOLE_1:10, XBOOLE_1:28
;
A27:
now reconsider loc =
IC (Comput (ProgramPart s1),s1,(i + 1)) as
Element of
NAT ;
assume A28:
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
;
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(i + 1))reconsider kk =
loc as
Element of
NAT ;
A29:
loc in dom (ProgramPart p)
by A2, A4, AMI_5:86;
ProgramPart p c= p
by RELAT_1:88;
then A30:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then
loc + k in dom (Relocated p,k)
by A29, AMISTD_2:71;
then A31:
(Relocated p,k) . (loc + k) =
s2 . (loc + k)
by A3, GRFUNC_1:8
.=
(Comput (ProgramPart s2),s2,(i + 1)) . (kk + k)
by AMI_1:54
;
Y:
(ProgramPart (Comput (ProgramPart s1),s1,(i + 1))) /. (IC (Comput (ProgramPart s1),s1,(i + 1))) = (Comput (ProgramPart s1),s1,(i + 1)) . (IC (Comput (ProgramPart s1),s1,(i + 1)))
by COMPOS_1:38;
TX:
ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,(i + 1))
by AMI_1:123;
TY:
ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(i + 1))
by AMI_1:123;
Z:
(ProgramPart s2) /. (IC (Comput (ProgramPart s2),s2,(i + 1))) = (Comput (ProgramPart s2),s2,(i + 1)) . (IC (Comput (ProgramPart s2),s2,(i + 1)))
by TY, COMPOS_1:38;
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,(i + 1)) =
s1 . loc
by Y, TX, AMI_1:54
.=
p . loc
by A2, A29, A30, GRFUNC_1:8
;
hence
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A28, A29, A31, Th27, Z;
verum end; set I =
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i);
A32:
Comput (ProgramPart s2),
s2,
(i + 1) =
Following (ProgramPart s2),
(Comput (ProgramPart s2),s2,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i)
;
A33:
dom (Comput (ProgramPart s2),s2,i) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT
by AMI_5:23, PARTFUN1:def 4;
A34:
dom (Comput (ProgramPart s1),s1,i) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT
by AMI_5:23, PARTFUN1:def 4;
A35:
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 A34, A25, XBOOLE_1:10, XBOOLE_1:28
;
A36:
Comput (ProgramPart s1),
(s1 +* (DataPart s2)),
(i + 1) =
Following (ProgramPart s1),
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i)
by A2, A4, A5, TX1, AMI_5:87
;
A37:
dom (DataPart p) = dom (DataPart (Relocated p,k))
by AMISTD_2:68;
then A38:
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 A10, A25, XBOOLE_1:10, XBOOLE_1:28
;
A39:
now let x be
set ;
for d being Data-Location 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 ;
( 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 A40:
(
d = x &
d in dom (DataPart p) )
and A41:
(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 A26, A40, A41, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A37, A38, A40, FUNCT_1:70
;
verum end; A42:
dom ((Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k)))) =
(dom (Comput (ProgramPart s2),s2,i)) /\ (dom (DataPart p))
by A37, RELAT_1:90
.=
dom (DataPart p)
by A33, A25, XBOOLE_1:10, XBOOLE_1:28
;
A43:
now let x be
set ;
for d being Data-Location 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 ;
( 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 A44:
d = x
and A45:
d in dom (DataPart p)
and A46:
(
(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))) . x
(
((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 A37, A35, A42, A45, FUNCT_1:70;
hence ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . d
by A8, A37, A26, A44, A45, A46, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A37, A38, A44, A45, FUNCT_1:70
;
verum end; reconsider j =
IC (Comput (ProgramPart s1),s1,i) as
Element of
NAT ;
A47:
Comput (ProgramPart s1),
s1,
(i + 1) =
Following (ProgramPart s1),
(Comput (ProgramPart s1),s1,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i)
;
A48:
succ ((IC (Comput (ProgramPart s1),s1,i)) + k) =
(j + k) + 1
by NAT_1:39
.=
(j + 1) + k
.=
(succ (IC (Comput (ProgramPart s1),s1,i))) + k
by NAT_1:39
;
per cases
( InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 0 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 1 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 2 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 3 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 4 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 5 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 6 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 7 or InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 8 )
by AMI_5:36, NAT_1:33;
suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 0
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then A49:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = halt SCM
by AMI_5:46;
then X:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i)
by A3, AMISTD_2:30;
then A50:
CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) = halt SCM
by A7, A49, AMI_5:37;
thus (IC (Comput (ProgramPart s1),s1,(i + 1))) + k =
(IC (Comput (ProgramPart s1),s1,i)) + k
by A47, A49, AMI_1:def 8
.=
IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A32, A50, AMI_1:def 8
;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )hence
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A27;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A51:
Comput (ProgramPart s2),
s2,
(i + 1) = Comput (ProgramPart s2),
s2,
i
by A32, A50, 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 A8, A47, A49, AMI_1:def 8;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))thus
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A9, A36, A49, A51, AMI_1:def 8;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 1
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider da,
db being
Data-Location such that A52:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = da := db
by AMI_5:47;
A53:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = da := db
by A52, AMISTD_2:29;
A54:
(Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A52, AMI_3:8;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A47, A32, A48, A53, AMI_3:8;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A27, A47, A32, A48, A53, A54, AMI_3:8;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A55:
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A22;
now
DataPart p c= p
by RELAT_1:88;
then A56:
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 A57:
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A57;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose A58:
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 A7, A47, A32, A52, A53, AMI_3:8;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A2, A4, A5, A26, A39, A52, A55, A57, A56, A58, TX1, T21, AMI_5:88;
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 A7, A47, A32, A52, A53, AMI_3:8;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, A57;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A59:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db )
by A7, A32, A36, A52, A53, AMI_3:8;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A22, A14, A59;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A7, A32, A36, A52, A53, AMI_3:8;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A59;
verum end; end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 2
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider da,
db being
Data-Location such that A60:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = AddTo da,
db
by AMI_5:48;
A61:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = AddTo da,
db
by A60, AMISTD_2:29;
A62:
(Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A60, AMI_3:9;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A47, A32, A48, A61, AMI_3:9;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A27, A47, A32, A48, A61, A62, AMI_3:9;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A63:
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A22;
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A65;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
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) . 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 A7, A47, A32, A60, A61, AMI_3:9;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A2, A4, A5, A26, A39, A60, A63, A65, A64, A66, T21, TX1, AMI_5:89;
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 A7, A47, A32, A60, A61, AMI_3:9;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, 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 A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A67:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 s1),(s1 +* (DataPart s2)),(i + 1)) . d = ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) + ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) )
by A7, A32, A36, A60, A61, AMI_3:9;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A63, A67;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A7, A32, A36, A60, A61, AMI_3:9;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A67;
verum end; end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 3
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider da,
db being
Data-Location such that A68:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = SubFrom da,
db
by AMI_5:49;
A69:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = SubFrom da,
db
by A68, AMISTD_2:29;
A70:
(Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A68, AMI_3:10;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A47, A32, A48, A69, AMI_3:10;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A27, A47, A32, A48, A69, A70, AMI_3:10;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A71:
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A22;
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A73;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
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 A7, A47, A32, A68, A69, AMI_3:10;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A2, A4, A5, A26, A39, A68, A71, A73, A72, A74, TX1, T21, AMI_5:90;
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 A7, A47, A32, A68, A69, AMI_3:10;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, 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 A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A75:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 s1),(s1 +* (DataPart s2)),(i + 1)) . d = ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) - ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) )
by A7, A32, A36, A68, A69, AMI_3:10;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A71, A75;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A7, A32, A36, A68, A69, AMI_3:10;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A75;
verum end; end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 4
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider da,
db being
Data-Location such that A76:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = MultBy da,
db
by AMI_5:50;
A77:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = MultBy da,
db
by A76, AMISTD_2:29;
A78:
(Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A76, AMI_3:11;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A47, A32, A48, A77, AMI_3:11;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A27, A47, A32, A48, A77, A78, AMI_3:11;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A79:
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A22;
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A81;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
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 A7, A47, A32, A76, A77, AMI_3:11;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A2, A4, A5, A26, A39, A76, A79, A81, A80, A82, T21, TX1, AMI_5:91;
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 A7, A47, A32, A76, A77, AMI_3:11;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, 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 A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A83:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 s1),(s1 +* (DataPart s2)),(i + 1)) . d = ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) * ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) )
by A7, A32, A36, A76, A77, AMI_3:11;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A79, A83;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A7, A32, A36, A76, A77, AMI_3:11;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A83;
verum end; end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 5
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider da,
db being
Data-Location such that A84:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = Divide da,
db
by AMI_5:51;
A85:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
k = Divide da,
db
by A84, AMISTD_2:29;
A86:
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db )
by A22;
now per cases
( da <> db or da = db )
;
suppose A87:
da <> db
;
( (IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A88:
(Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A84, AMI_3:12;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A47, A32, A48, A85, AMI_3:12;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A27, A47, A32, A48, A85, A88, AMI_3:12;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now
DataPart p c= p
by RELAT_1:88;
then A89:
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 A90:
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A90;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
per cases
( da = d or db = d or ( da <> d & db <> d ) )
;
suppose A91:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then A92:
(
(Comput (ProgramPart s1),s1,(i + 1)) . d = ((Comput (ProgramPart s1),s1,i) . da) div ((Comput (ProgramPart s1),s1,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) div ((Comput (ProgramPart s2),s2,i) . db) )
by A7, A47, A32, A84, A85, A87, AMI_3:12;
((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) div ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) = ((Comput (ProgramPart s1),s1,i) . da) div ((Comput (ProgramPart s1),s1,i) . db)
by A2, A4, A5, A26, A84, A87, A90, A89, A91, TX1, AMI_5:92;
hence ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . d
by A86, A90, A92, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A37, A26, A38, A90, FUNCT_1:70
;
verum end; suppose A93:
db = 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) mod ((Comput (ProgramPart s1),s1,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db) )
by A7, A47, A32, A84, A85, AMI_3:12;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A2, A4, A5, A26, A39, A84, A86, A90, A89, A93, T21, TX1, AMI_5:93;
verum end; suppose
(
da <> d &
db <> 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 A7, A47, A32, A84, A85, AMI_3:12;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, A90;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A94:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
per cases
( da = d or db = d or ( da <> d & db <> d ) )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) div ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) div ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) )
by A7, A32, A36, A84, A85, A87, AMI_3:12;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A86, A94;
verum end; suppose
db = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) mod ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) )
by A7, A32, A36, A84, A85, AMI_3:12;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A86, A94;
verum end; suppose
(
da <> d &
db <> d )
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A7, A32, A36, A84, A85, AMI_3:12;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A94;
verum end; end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose A95:
da = db
;
( (IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A96:
(Exec (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A84, AMI_3:12;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A47, A32, A48, A85, AMI_3:12;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A6, A7, A27, A47, A32, A48, A85, A96, AMI_3:12;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 A97:
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A97;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose A98:
da = d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1A99:
(
((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 A37, A26, A35, A42, A97, FUNCT_1:70;
A100:
(
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . d = (Comput (ProgramPart s1),s1,(i + 1)) . d &
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . d = (Comput (ProgramPart s2),s2,(i + 1)) . d )
by A37, A26, A38, A97, FUNCT_1:70;
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db)
by A7, A32, A85, A95, A98, AMI_3:12;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A8, A37, A47, A84, A95, A98, A99, A100, AMI_3:12;
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 A7, A47, A32, A84, A85, A95, AMI_3:12;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, A97;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A101:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s2),s2,(i + 1)) . d = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da) mod ((Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . db) )
by A7, A32, A36, A84, A85, A95, AMI_3:12;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A14, A86, A101;
verum end; suppose
da <> d
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A7, A32, A36, A84, A85, A95, AMI_3:12;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A101;
verum end; end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; hence
(
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1)) &
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )
;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 6
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider loc being
Element of
NAT such that A102:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = SCM-goto loc
by AMI_5:52;
A103:
CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) = SCM-goto (loc + k)
by A7, A102, Th10;
thus (IC (Comput (ProgramPart s1),s1,(i + 1))) + k =
loc + k
by A47, A102, AMI_3:13
.=
IC (Comput (ProgramPart s2),s2,(i + 1))
by A32, A103, AMI_3:13
;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )hence
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A27;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 A104:
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A104;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
(
(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 A47, A32, A102, A103, AMI_3:13;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, A104;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A105:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A32, A36, A102, A103, AMI_3:13;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A105;
verum end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 7
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider loc being
Element of
NAT ,
da being
Data-Location such that A106:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = da =0_goto loc
by AMI_5:53;
A108:
CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) = da =0_goto (loc + k)
by A7, A106, Th11;
A110:
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A22;
A111:
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 = IC (Comput (ProgramPart s2),s2,(i + 1))hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A2, A4, A5, A106, A110, A107, A109, TX1, AMI_5:94;
verum end; hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A27, A111;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 A112:
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A112;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
(
(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 A47, A32, A106, A108, AMI_3:14;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, A112;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A113:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A32, A36, A106, A108, AMI_3:14;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A113;
verum end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)) = 8
;
( (IC (Comput (ProgramPart s1),s1,(b1 + 1))) + k = IC (Comput (ProgramPart s2),s2,(b1 + 1)) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(b1 + 1))),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(b1 + 1)) & (Comput (ProgramPart s1),s1,(b1 + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(b1 + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(b1 + 1)) = DataPart (Comput (ProgramPart s2),s2,(b1 + 1)) )then consider loc being
Element of
NAT ,
da being
Data-Location such that A114:
CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) = da >0_goto loc
by AMI_5:54;
A116:
CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) = da >0_goto (loc + k)
by A7, A114, Th12;
A118:
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A22;
A119:
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 = IC (Comput (ProgramPart s2),s2,(i + 1))hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A2, A4, A5, A114, A118, A115, A117, TX1, AMI_5:95;
verum end; hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart s2),(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 s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,(i + 1))
by A27, A119;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(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 A120:
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 AMI_3:72, RELAT_1:87;
then
x in SCM-Data-Loc
by A26, A120;
then reconsider d =
x as
Data-Location by AMI_3:def 2;
(
(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 A47, A32, A114, A116, AMI_3:15;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A26, A43, A120;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A37, A26, A38, 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 A37, A26, A38, GRFUNC_1:9;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A121:
x in dom (DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen reconsider d =
x as
Data-Location by A12, AMI_3:def 2;
(
(Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) . d &
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d )
by A32, A36, A114, A116, AMI_3:15;
hence
(DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A18, A121;
verum end; then
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A12, A13, GRFUNC_1:9;
verum end; end;
then A122:
for i being Element of NAT st S1[i] holds
S1[i + 1]
;
A123:
DataPart p c= p
by RELAT_1:88;
A124:
DataPart (Relocated p,k) c= Relocated p,k
by RELAT_1:88;
A125:
DataPart p = DataPart (Relocated p,k)
by AMISTD_2:68;
A126:
IC SCM in dom (Relocated p,k)
by AMISTD_2:72;
now thus (IC (Comput (ProgramPart s1),s1,0 )) + k =
(IC s1) + k
by AMI_1:13
.=
(IC p) + k
by A1, A2, GRFUNC_1:8
.=
IC (Relocated p,k)
by A1, Th26
.=
IC s2
by A3, A126, GRFUNC_1:8
.=
IC (Comput (ProgramPart s2),s2,0 )
by AMI_1:13
;
( IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,0 )),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,0 ) & (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),0 ) = DataPart (Comput (ProgramPart s2),s2,0 ) )reconsider loc =
IC p as
Element of
NAT ;
Z:
Comput (ProgramPart s1),
s1,
0 = s1
by AMI_1:13;
Y:
(ProgramPart (Comput (ProgramPart s1),s1,0 )) /. (IC (Comput (ProgramPart s1),s1,0 )) = (Comput (ProgramPart s1),s1,0 ) . (IC (Comput (ProgramPart s1),s1,0 ))
by COMPOS_1:38;
A127:
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,0 )),
k =
IncAddr (CurInstr (ProgramPart s1),s1),
k
by Z
.=
IncAddr (s1 . (IC s1)),
k
by Y, Z
;
A128:
IC p = IC s1
by A1, A2, GRFUNC_1:8;
then
IC p = IC (Comput (ProgramPart s1),s1,0 )
by AMI_1:13;
then A129:
loc in dom (ProgramPart p)
by A2, A4, AMI_5:86;
ProgramPart p c= p
by RELAT_1:88;
then A130:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then A131:
(IC p) + k in dom (Relocated p,k)
by A129, AMISTD_2:71;
A132:
IC SCM in dom (Relocated p,k)
by AMISTD_2:72;
A133:
p . (IC p) = s1 . (IC s1)
by A2, A128, A129, A130, GRFUNC_1:8;
Z:
Comput (ProgramPart s2),
s2,
0 = s2
by AMI_1:13;
Y:
(ProgramPart (Comput (ProgramPart s2),s2,0 )) /. (IC (Comput (ProgramPart s2),s2,0 )) = (Comput (ProgramPart s2),s2,0 ) . (IC (Comput (ProgramPart s2),s2,0 ))
by COMPOS_1:38;
CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,0 ) =
CurInstr (ProgramPart s2),
s2
by Z
.=
s2 . (IC (Relocated p,k))
by A3, A132, Y, Z, GRFUNC_1:8
.=
s2 . ((IC p) + k)
by A1, Th26
.=
(Relocated p,k) . ((IC p) + k)
by A3, A131, GRFUNC_1:8
;
hence
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,0 )),
k = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,0 )
by A129, A133, A127, Th27;
( (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),0 ) = DataPart (Comput (ProgramPart s2),s2,0 ) )A134:
dom (DataPart s2) = SCM-Data-Loc
by AMI_3:72, COMPOS_1:50;
thus (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
by AMI_1:13
.=
DataPart p
by A2, A123, GRFUNC_1:64, XBOOLE_1:1
.=
s2 | (dom (DataPart p))
by A3, A125, A124, GRFUNC_1:64, XBOOLE_1:1
.=
(Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k)))
by A125, AMI_1:13
;
DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),0 ) = DataPart (Comput (ProgramPart s2),s2,0 )thus DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),0 ) =
DataPart (s1 +* (DataPart s2))
by AMI_1:13
.=
DataPart s2
by A134, AMI_3:72, FUNCT_4:24
.=
DataPart (Comput (ProgramPart s2),s2,0 )
by AMI_1:13
;
verum end;
then A135:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A135, A122); verum