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));
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)} \/ (Data-Locations SCM)) \/ 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))) = Data-Locations SCM
by COMPOS_1:50;
A12:
dom (DataPart (Comput ((ProgramPart s1),(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations SCM
by COMPOS_1:50;
A13:
dom (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) = Data-Locations SCM
by 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))) = Data-Locations SCM
by 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)} \/ (Data-Locations SCM)) \/ NAT
by AMI_5:23, PARTFUN1:def 4;
dom (DataPart p) = (dom p) /\ (Data-Locations SCM)
by RELAT_1:90;
then A25:
dom (DataPart p) c= {(IC SCM)} \/ (Data-Locations SCM)
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, COMPOS_1:118;
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
;
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 COMPOS_1:38
.=
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 EXTPRO_1:4
.=
Exec (
(CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i)))),
(Comput ((ProgramPart s2),s2,i)))
;
A33:
dom (Comput ((ProgramPart s2),s2,i)) = ({(IC SCM)} \/ (Data-Locations SCM)) \/ NAT
by AMI_5:23, PARTFUN1:def 4;
A34:
dom (Comput ((ProgramPart s1),s1,i)) = ({(IC SCM)} \/ (Data-Locations SCM)) \/ 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 EXTPRO_1:4
.=
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 COMPOS_1:115;
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 EXTPRO_1:4
.=
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 A50:
CurInstr (
(ProgramPart s2),
(Comput ((ProgramPart s2),s2,i)))
= halt SCM
by A7, COMPOS_1:93;
thus (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k =
(IC (Comput ((ProgramPart s1),s1,i))) + k
by A47, A49, EXTPRO_1:def 3
.=
IC (Comput ((ProgramPart s2),s2,(i + 1)))
by A6, A32, A50, EXTPRO_1:def 3
;
( 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, EXTPRO_1:def 3;
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, EXTPRO_1:def 3;
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, EXTPRO_1:def 3;
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, COMPOS_1:92;
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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A57;
then reconsider d =
x as
Data-Location by AMI_3:72, 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, 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:72, 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, COMPOS_1:92;
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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A65;
then reconsider d =
x as
Data-Location by AMI_3:72, 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, 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:72, 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, COMPOS_1:92;
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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A73;
then reconsider d =
x as
Data-Location by AMI_3:72, 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, 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:72, 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, COMPOS_1:92;
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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A81;
then reconsider d =
x as
Data-Location by AMI_3:72, 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, 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:72, 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, COMPOS_1:92;
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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A90;
then reconsider d =
x as
Data-Location by AMI_3:72, 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, 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:72, 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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A97;
then reconsider d =
x as
Data-Location by AMI_3:72, 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:72, 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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A104;
then reconsider d =
x as
Data-Location by AMI_3:72, 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:72, 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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A112;
then reconsider d =
x as
Data-Location by AMI_3:72, 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:72, 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= Data-Locations SCM
by RELAT_1:87;
then
x in Data-Locations SCM
by A26, A120;
then reconsider d =
x as
Data-Location by AMI_3:72, 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:72, 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 COMPOS_1:115;
A126:
IC SCM in dom (Relocated (p,k))
by COMPOS_1:119;
now thus (IC (Comput ((ProgramPart s1),s1,0))) + k =
(IC s1) + k
by EXTPRO_1:3
.=
(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 EXTPRO_1:3
;
( 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 ;
U1:
ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,0))
by AMI_1:123;
Z:
Comput (
(ProgramPart s1),
s1,
0)
= s1
by EXTPRO_1:3;
Y:
(ProgramPart s1) /. (IC (Comput ((ProgramPart s1),s1,0))) = (Comput ((ProgramPart s1),s1,0)) . (IC (Comput ((ProgramPart s1),s1,0)))
by U1, COMPOS_1:38;
A127:
IncAddr (
(CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,0)))),
k) =
IncAddr (
(CurInstr ((ProgramPart s1),s1)),
k)
by EXTPRO_1:3
.=
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 EXTPRO_1:3;
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, COMPOS_1:118;
A132:
IC SCM in dom (Relocated (p,k))
by COMPOS_1:119;
A133:
p . (IC p) = s1 . (IC s1)
by A2, A128, A129, A130, GRFUNC_1:8;
U2:
ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,0))
by AMI_1:123;
Z:
Comput (
(ProgramPart s2),
s2,
0)
= s2
by EXTPRO_1:3;
Y:
(ProgramPart s2) /. (IC (Comput ((ProgramPart s2),s2,0))) = (Comput ((ProgramPart s2),s2,0)) . (IC (Comput ((ProgramPart s2),s2,0)))
by U2, COMPOS_1:38;
CurInstr (
(ProgramPart s2),
(Comput ((ProgramPart s2),s2,0))) =
CurInstr (
(ProgramPart s2),
s2)
by EXTPRO_1:3
.=
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) = Data-Locations SCM
by COMPOS_1:50;
thus (Comput ((ProgramPart s1),s1,0)) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
by EXTPRO_1:3
.=
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, EXTPRO_1:3
;
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 EXTPRO_1:3
.=
DataPart s2
by A134, FUNCT_4:24
.=
DataPart (Comput ((ProgramPart s2),s2,0))
by EXTPRO_1:3
;
verum end;
then A135:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A135, A122); verum