let k be Nat; for R being non trivial Ring
for s1, s2 being State of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function
for p being non empty b4 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let R be non trivial Ring; for s1, s2 being State of (SCM R)
for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let s1, s2 be State of (SCM R); for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let p be non empty q -autonomic FinPartState of (SCM R); ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) )
assume that
A1:
p c= s1
and
A2:
IncIC (p,k) c= s2
; for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
A3:
IC in dom p
by AMISTD_5:6;
let P1, P2 be Instruction-Sequence of (SCM R); ( q c= P1 & Reloc (q,k) c= P2 implies for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) )
assume A4:
( q c= P1 & Reloc (q,k) c= P2 )
; for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
set s = s1 +* (DataPart s2);
defpred S1[ Nat] means ( (IC (Comput (P1,s1,$1))) + k = IC (Comput (P2,s2,$1)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,$1)))),k) = CurInstr (P2,(Comput (P2,s2,$1))) & (Comput (P1,s1,$1)) | (dom (DataPart p)) = (Comput (P2,s2,$1)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),$1)) = DataPart (Comput (P2,s2,$1)) );
A5:
IC p = IC s1
by A1, A3, GRFUNC_1:2;
then
IC p = IC (Comput (P1,s1,0))
;
then A6:
IC p in dom q
by A1, A4, AMISTD_5:def 4;
A7:
p c= s1 +* (DataPart s2)
by A1, A2, MEMSTR_0:61;
A8:
for i being Nat st S1[i] holds
S1[i + 1]
proof
set DPp =
DataPart p;
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A9:
(IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i))
and A10:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= CurInstr (
P2,
(Comput (P2,s2,i)))
and A11:
(Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
and A12:
DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i))
;
S1[i + 1]
set Cs2i1 =
Comput (
P2,
s2,
(i + 1));
set Cs3i =
Comput (
P1,
(s1 +* (DataPart s2)),
i);
set Cs2i =
Comput (
P2,
s2,
i);
A13:
Comput (
P2,
s2,
(i + 1)) =
Following (
P2,
(Comput (P2,s2,i)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P2,(Comput (P2,s2,i)))),
(Comput (P2,s2,i)))
;
A15:
now for d being Data-Location of R holds (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dlet d be
Data-Location of
R;
(Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dA16:
d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i)))
by A14;
hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d =
(DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d
by FUNCT_1:47
.=
(Comput (P2,s2,i)) . d
by A12, A16, FUNCT_1:47
;
verum end;
set Cs1i1 =
Comput (
P1,
s1,
(i + 1));
set Cs1i =
Comput (
P1,
s1,
i);
dom (Comput (P1,s1,(i + 1))) = the
carrier of
(SCM R)
by PARTFUN1:def 2;
then A17:
dom (Comput (P1,s1,(i + 1))) = {(IC )} \/ (Data-Locations )
by XBOOLE_1:45;
A18:
((IC (Comput (P1,s1,i))) + k) + 1
= ((IC (Comput (P1,s1,i))) + 1) + k
;
A19:
now ( (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) implies IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) )reconsider loc =
IC (Comput (P1,s1,(i + 1))) as
Element of
NAT ;
assume A20:
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
;
IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))A21:
loc in dom q
by A1, A4, AMISTD_5:def 4;
loc + k in dom (Reloc (q,k))
by A21, COMPOS_1:46;
then A22:
(Reloc (q,k)) . (loc + k) = P2 . (loc + k)
by A4, GRFUNC_1:2;
A23:
P2 /. (IC (Comput (P2,s2,(i + 1)))) = P2 . (IC (Comput (P2,s2,(i + 1))))
by PBOOLE:143;
CurInstr (
P1,
(Comput (P1,s1,(i + 1)))) =
P1 . loc
by PBOOLE:143
.=
q . loc
by A21, A4, GRFUNC_1:2
;
hence
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A20, A21, A22, A23, COMPOS_1:35;
verum end;
dom (Comput (P2,s2,i)) = the
carrier of
(SCM R)
by PARTFUN1:def 2;
then A24:
dom (Comput (P2,s2,i)) = {(IC )} \/ (Data-Locations )
by XBOOLE_1:45;
dom (DataPart p) = (dom p) /\ (Data-Locations )
by RELAT_1:61;
then A25:
dom (DataPart p) c= {(IC )} \/ (Data-Locations )
by XBOOLE_1:10, XBOOLE_1:17;
set Cs3i1 =
Comput (
P1,
(s1 +* (DataPart s2)),
(i + 1));
A26:
dom (DataPart (Comput (P2,s2,i))) = Data-Locations
by MEMSTR_0:9;
A27:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations
by MEMSTR_0:9;
then A28:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) c= dom (DataPart (Comput (P2,s2,(i + 1))))
by MEMSTR_0:9;
A29:
dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations
by MEMSTR_0:9;
A30:
now for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
set ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )assume that A31:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
and A32:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xthus (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x =
(Comput (P2,s2,(i + 1))) . x
by A31, A32, FUNCT_1:47
.=
(DataPart (Comput (P2,s2,(i + 1)))) . x
by A27, A29, A31, FUNCT_1:47
;
verum end;
A33:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations
by MEMSTR_0:9;
A34:
now for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
set ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )assume that A35:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
and A36:
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x &
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
(DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x
by A33, A27, A35, FUNCT_1:47;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A12, A26, A27, A30, A35, A36, FUNCT_1:47;
verum end;
dom (Comput (P1,s1,i)) = the
carrier of
(SCM R)
by PARTFUN1:def 2;
then A37:
dom (Comput (P1,s1,i)) = {(IC )} \/ (Data-Locations )
by XBOOLE_1:45;
dom (Comput (P2,s2,(i + 1))) = the
carrier of
(SCM R)
by PARTFUN1:def 2;
then A38:
dom (Comput (P2,s2,(i + 1))) = {(IC )} \/ (Data-Locations )
by XBOOLE_1:45;
set I =
CurInstr (
P1,
(Comput (P1,s1,i)));
A39:
Comput (
P1,
s1,
(i + 1)) =
Following (
P1,
(Comput (P1,s1,i)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P1,(Comput (P1,s1,i)))),
(Comput (P1,s1,i)))
;
A40:
dom ((Comput (P1,s1,i)) | (dom (DataPart p))) =
(dom (Comput (P1,s1,i))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A37, A25, XBOOLE_1:28
;
A41:
dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) =
(dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A17, A25, XBOOLE_1:28
;
A42:
dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) =
(dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A38, A25, XBOOLE_1:28
;
then A43:
dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) c= dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p)))
by A41;
A44:
dom ((Comput (P2,s2,i)) | (dom (DataPart p))) =
(dom (Comput (P2,s2,i))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A24, A25, XBOOLE_1:28
;
A45:
now for x being set
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet x be
set ;
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet d be
Data-Location of
R;
( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )assume that A46:
d = x
and A47:
d in dom (DataPart p)
and A48:
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xA49:
(
((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d &
((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d )
by A40, A44, A47, FUNCT_1:47;
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P1,s1,(i + 1))) . d
by A41, A46, A47, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A11, A42, A46, A47, A48, A49, FUNCT_1:47
;
verum end;
A50:
now for x being set
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet x be
set ;
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet d be
Data-Location of
R;
( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )assume that A51:
(
d = x &
d in dom (DataPart p) )
and A52:
(Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xthus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P2,s2,(i + 1))) . d
by A41, A51, A52, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A42, A51, FUNCT_1:47
;
verum end;
A53:
Comput (
P1,
(s1 +* (DataPart s2)),
(i + 1)) =
Following (
P1,
(Comput (P1,(s1 +* (DataPart s2)),i)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P1,(Comput (P1,s1,i)))),
(Comput (P1,(s1 +* (DataPart s2)),i)))
by A1, A7, A4, AMISTD_5:7
;
not not
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 & ... & not
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7
by SCMRING3:39;
per cases then
( InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 )
;
suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0
;
S1[i + 1]then A54:
CurInstr (
P1,
(Comput (P1,s1,i)))
= halt (SCM R)
by SCMRING3:12;
hence (IC (Comput (P1,s1,(i + 1)))) + k =
(IC (Comput (P1,s1,i))) + k
by A39, EXTPRO_1:def 3
.=
IC (Comput (P2,s2,(i + 1)))
by A9, A10, A13, A54, EXTPRO_1:def 3
;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )hence
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A19;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )A55:
Comput (
P2,
s2,
(i + 1))
= Comput (
P2,
s2,
i)
by A10, A13, A54, EXTPRO_1:def 3;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A11, A39, A54, EXTPRO_1:def 3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))thus
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A12, A53, A54, A55, EXTPRO_1:def 3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A56:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := db
by SCMRING3:13;
A57:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= da := db
by A56, COMPOS_0:4;
A58:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A56, SCMRING2:11;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A39, A13, A18, A57, SCMRING2:11;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A9, A10, A19, A39, A13, A18, A57, A58, SCMRING2:11;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )A59:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A15;
now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p
by RELAT_1:59;
then A60:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
let x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )assume A61:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A61, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose A62:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . db &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db )
by A10, A39, A13, A56, A57, SCMRING2:11;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A7, A41, A50, A56, A59, A61, A60, A62, Th7, A4;
verum end; suppose
da <> d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A39, A13, A56, A57, SCMRING2:11;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A61;
verum end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )assume A63:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . db )
by A10, A13, A53, A56, A57, SCMRING2:11;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A15, A30, A63;
verum end; suppose
da <> d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A13, A53, A56, A57, SCMRING2:11;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A63;
verum end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A64:
CurInstr (
P1,
(Comput (P1,s1,i)))
= AddTo (
da,
db)
by SCMRING3:14;
A65:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= AddTo (
da,
db)
by A64, COMPOS_0:4;
A66:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A64, SCMRING2:12;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A39, A13, A18, A65, SCMRING2:12;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A9, A10, A19, A39, A13, A18, A65, A66, SCMRING2:12;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )A67:
(
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da &
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db )
by A15;
now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p
by RELAT_1:59;
then A68:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
let x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )assume A69:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A69, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose A70:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) &
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
by A10, A39, A13, A64, A65, SCMRING2:12;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A7, A41, A50, A64, A67, A69, A68, A70, Th8, A4;
verum end; suppose
da <> d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A39, A13, A64, A65, SCMRING2:12;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A69;
verum end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )assume A71:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) )
by A10, A13, A53, A64, A65, SCMRING2:12;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A30, A67, A71;
verum end; suppose
da <> d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A13, A53, A64, A65, SCMRING2:12;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A71;
verum end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A72:
CurInstr (
P1,
(Comput (P1,s1,i)))
= SubFrom (
da,
db)
by SCMRING3:15;
A73:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= SubFrom (
da,
db)
by A72, COMPOS_0:4;
A74:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A72, SCMRING2:13;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A39, A13, A18, A73, SCMRING2:13;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A9, A10, A19, A39, A13, A18, A73, A74, SCMRING2:13;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )A75:
(
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da &
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db )
by A15;
now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p
by RELAT_1:59;
then A76:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
let x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )assume A77:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A77, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose A78:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) &
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
by A10, A39, A13, A72, A73, SCMRING2:13;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A7, A41, A50, A72, A75, A77, A76, A78, Th9, A4;
verum end; suppose
da <> d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A39, A13, A72, A73, SCMRING2:13;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A77;
verum end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )assume A79:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) )
by A10, A13, A53, A72, A73, SCMRING2:13;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A30, A75, A79;
verum end; suppose
da <> d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A13, A53, A72, A73, SCMRING2:13;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A79;
verum end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4
;
S1[i + 1]then consider da,
db being
Data-Location of
R such that A80:
CurInstr (
P1,
(Comput (P1,s1,i)))
= MultBy (
da,
db)
by SCMRING3:16;
A81:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= MultBy (
da,
db)
by A80, COMPOS_0:4;
A82:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A80, SCMRING2:14;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A39, A13, A18, A81, SCMRING2:14;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A9, A10, A19, A39, A13, A18, A81, A82, SCMRING2:14;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )A83:
(
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da &
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db )
by A15;
now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p
by RELAT_1:59;
then A84:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
let x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )assume A85:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A85, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose A86:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) &
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
by A10, A39, A13, A80, A81, SCMRING2:14;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A7, A41, A50, A80, A83, A85, A84, A86, Th10, A4;
verum end; suppose
da <> d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A39, A13, A80, A81, SCMRING2:14;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A85;
verum end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )assume A87:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) )
by A10, A13, A53, A80, A81, SCMRING2:14;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A30, A83, A87;
verum end; suppose
da <> d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A13, A53, A80, A81, SCMRING2:14;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A87;
verum end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5
;
S1[i + 1]then consider da being
Data-Location of
R,
r being
Element of
R such that A88:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := r
by SCMRING3:17;
A89:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= da := r
by A88, COMPOS_0:4;
A90:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A88, SCMRING2:17;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A39, A13, A18, A89, SCMRING2:17;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A9, A10, A19, A39, A13, A18, A89, A90, SCMRING2:17;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )assume A91:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A91, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose A92:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P1,s1,(i + 1))) . d
by A41, A91, FUNCT_1:49
.=
r
by A39, A88, A92, SCMRING2:17
.=
(Comput (P2,s2,(i + 1))) . d
by A10, A13, A89, A92, SCMRING2:17
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A91, FUNCT_1:49
;
verum end; suppose
da <> d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A39, A13, A88, A89, SCMRING2:17;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A91;
verum end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )assume A93:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
per cases
( da = d or da <> d )
;
suppose
da = d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P2,s2,(i + 1))) . d = r &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = r )
by A10, A13, A53, A88, A89, SCMRING2:17;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A30, A93;
verum end; suppose
da <> d
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A10, A13, A53, A88, A89, SCMRING2:17;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A93;
verum end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6
;
S1[i + 1]then consider loc being
Nat such that A94:
CurInstr (
P1,
(Comput (P1,s1,i)))
= goto (
loc,
R)
by SCMRING3:18;
A95:
CurInstr (
P2,
(Comput (P2,s2,i)))
= goto (
(loc + k),
R)
by A10, A94, SCMRING3:37;
thus (IC (Comput (P1,s1,(i + 1)))) + k =
loc + k
by A39, A94, SCMRING2:15
.=
IC (Comput (P2,s2,(i + 1)))
by A13, A95, SCMRING2:15
;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )hence
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A19;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )assume A96:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A96, SCMRING2:23;
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A39, A13, A94, A95, SCMRING2:15;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A96;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )assume A97:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xthen reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A13, A53, A94, A95, SCMRING2:15;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A97;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7
;
S1[i + 1]then consider da being
Data-Location of
R,
loc being
Nat such that A98:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da =0_goto loc
by SCMRING3:19;
A99:
now ( ( (Comput (P1,s1,i)) . da = 0. R & (IC (Comput (P1,s1,(i + 1)))) + k = loc + k ) or ( (Comput (P1,s1,i)) . da <> 0. R & (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 ) )end; A100:
CurInstr (
P2,
(Comput (P2,s2,i)))
= da =0_goto (loc + k)
by A10, A98, SCMRING3:38;
A101:
now ( ( (Comput (P2,s2,i)) . da = 0. R & IC (Comput (P2,s2,(i + 1))) = loc + k ) or ( (Comput (P2,s2,i)) . da <> 0. R & IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 ) )end; A102:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A15;
now (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))per cases
( loc <> (IC (Comput (P1,s1,i))) + 1 or loc = (IC (Comput (P1,s1,i))) + 1 )
;
suppose
loc <> (IC (Comput (P1,s1,i))) + 1
;
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A1, A7, A98, A102, A99, A101, Th11, A4;
verum end; hence
(
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) &
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1)))) )
by A19;
( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )now for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . xlet x be
object ;
( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )assume A103:
x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p)))
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d =
x as
Data-Location of
R by A41, A103, SCMRING2:23;
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A39, A13, A98, A100, SCMRING2:16;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A45, A103;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A41, A42, GRFUNC_1:3;
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))now for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xlet x be
object ;
( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )assume A104:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . xthen reconsider d =
x as
Data-Location of
R by A27, SCMRING2:23;
(
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A13, A53, A98, A100, SCMRING2:16;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A104;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A28, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A27, A29, GRFUNC_1:3;
verum end;
end;
A105:
DataPart p c= p
by RELAT_1:59;
A106:
DataPart (IncIC (p,k)) = DataPart p
by MEMSTR_0:51;
A107:
DataPart p c= IncIC (p,k)
by A106, MEMSTR_0:12;
A108: (Comput (P1,s1,0)) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
.=
DataPart p
by A1, A105, GRFUNC_1:23, XBOOLE_1:1
.=
s2 | (dom (DataPart p))
by A107, A2, GRFUNC_1:23, XBOOLE_1:1
.=
(Comput (P2,s2,0)) | (dom (DataPart p))
;
A109: DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) =
DataPart (s1 +* (DataPart s2))
.=
DataPart s2
by PBOOLE:142
.=
DataPart (Comput (P2,s2,0))
;
A110:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
A111: (IC (Comput (P1,s1,0))) + k =
(IC s1) + k
.=
(IC p) + k
by A1, A3, GRFUNC_1:2
.=
(IC p) + k
.=
IC (IncIC (p,k))
by MEMSTR_0:53
.=
IC s2
by A2, A110, GRFUNC_1:2
.=
IC (Comput (P2,s2,0))
;
A112:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
A113:
(IC p) + k in dom (Reloc (q,k))
by A6, COMPOS_1:46;
A114:
P2 /. (IC s2) = P2 . (IC s2)
by PBOOLE:143;
A115: CurInstr (P2,(Comput (P2,s2,0))) =
P2 . (IC s2)
by A114
.=
P2 . (IC (IncIC (p,k)))
by A2, A112, GRFUNC_1:2
.=
P2 . ((IC p) + k)
by MEMSTR_0:53
.=
P2 . ((IC p) + k)
.=
(Reloc (q,k)) . ((IC p) + k)
by A113, A4, GRFUNC_1:2
;
A116:
q . (IC p) = P1 . (IC s1)
by A5, A6, A4, GRFUNC_1:2;
A117:
CurInstr (P1,s1) = q . (IC p)
by A116, PBOOLE:143;
A118: IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) =
IncAddr ((CurInstr (P1,s1)),k)
.=
CurInstr (P2,(Comput (P2,s2,0)))
by A115, A6, A117, COMPOS_1:35
;
A119:
S1[ 0 ]
by A111, A118, A108, A109;
for n being Nat holds S1[n]
from NAT_1:sch 2(A119, A8);
hence
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
; verum