let k be Nat; for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM 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 -valued finite non halt-free Function; for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM 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; for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM 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; ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of SCM 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 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;
A4:
p c= s1
by A1;
let P1, P2 be Instruction-Sequence of SCM; ( 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 A5:
( 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)) )
A6:
Reloc (q,k) c= P2
by A5;
A7:
q c= P1
by A5;
set s3 = 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)) );
A8:
p c= s1 +* (DataPart s2)
by A1, A2, MEMSTR_0:61;
A9:
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 A10:
(IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i))
and A11:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= CurInstr (
P2,
(Comput (P2,s2,i)))
and A12:
(Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
and A13:
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);
dom (Comput (P2,s2,(i + 1))) = the
carrier of
SCM
by PARTFUN1:def 2;
then A14:
dom (Comput (P2,s2,(i + 1))) = {(IC )} \/ (Data-Locations )
by STRUCT_0:4;
set Cs3i1 =
Comput (
P1,
(s1 +* (DataPart s2)),
(i + 1));
A15:
dom (DataPart (Comput (P2,s2,i))) = Data-Locations
by MEMSTR_0:9;
A16:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations
by MEMSTR_0:9;
A17:
dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations
by MEMSTR_0:9;
A18:
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 A19:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
and A20:
(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 A19, A20, FUNCT_1:47
.=
(DataPart (Comput (P2,s2,(i + 1)))) . x
by A16, A17, A19, FUNCT_1:47
;
verum end;
A21:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations
by MEMSTR_0:9;
A22:
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 A23:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
and A24:
(
(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 A21, A16, A23, FUNCT_1:47;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A13, A15, A16, A18, A23, A24, FUNCT_1:47;
verum end;
A26:
now for d being Data-Location holds (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dlet d be
Data-Location;
(Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dA27:
d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i)))
by A25;
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 A13, A27, 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
by PARTFUN1:def 2;
then A28:
dom (Comput (P1,s1,(i + 1))) = {(IC )} \/ (Data-Locations )
by STRUCT_0:4;
dom (DataPart p) = (dom p) /\ (Data-Locations )
by RELAT_1:61;
then A29:
dom (DataPart p) c= {(IC )} \/ (Data-Locations )
by XBOOLE_1:10, XBOOLE_1:17;
A30:
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 A28, A29, XBOOLE_1:28
;
A31:
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 A32:
(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))))reconsider kk =
loc as
Element of
NAT ;
A33:
loc in dom q
by A7, A4, AMISTD_5:def 4;
A34:
loc + k in dom (Reloc (q,k))
by A33, COMPOS_1:46;
A35:
dom P2 = NAT
by PARTFUN1:def 2;
dom P1 = NAT
by PARTFUN1:def 2;
then CurInstr (
P1,
(Comput (P1,s1,(i + 1)))) =
P1 . loc
by PARTFUN1:def 6
.=
q . loc
by A33, A5, GRFUNC_1:2
.=
q . loc
;
hence IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k) =
(Reloc (q,k)) . (loc + k)
by A33, COMPOS_1:35
.=
P2 . (IC (Comput (P2,s2,(i + 1))))
by A32, A34, A6, GRFUNC_1:2
.=
CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A35, PARTFUN1:def 6
;
verum end;
set I =
CurInstr (
P1,
(Comput (P1,s1,i)));
A36:
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)))
;
dom (Comput (P2,s2,i)) = the
carrier of
SCM
by PARTFUN1:def 2;
then A37:
dom (Comput (P2,s2,i)) = {(IC )} \/ (Data-Locations )
by STRUCT_0:4;
dom (Comput (P1,s1,i)) = the
carrier of
SCM
by PARTFUN1:def 2;
then A38:
dom (Comput (P1,s1,i)) = {(IC )} \/ (Data-Locations )
by STRUCT_0:4;
A39:
dom ((Comput (P1,s1,i)) | (dom (DataPart p))) =
(dom (Comput (P1,s1,i))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A38, A29, XBOOLE_1:28
;
A40:
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, A8, A5, AMISTD_5:7
;
A41:
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 A14, A29, XBOOLE_1:28
;
A42:
now for x being set
for d being Data-Location 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 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;
( 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 A43:
(
d = x &
d in dom (DataPart p) )
and A44:
(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 A30, A43, A44, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A43, FUNCT_1:47
;
verum end;
A45:
dom ((Comput (P2,s2,i)) | (dom (DataPart p))) =
(dom (Comput (P2,s2,i))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A37, A29, XBOOLE_1:28
;
A46:
now for x being set
for d being Data-Location 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 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;
( 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 A47:
d = x
and A48:
d in dom (DataPart p)
and A49:
(
(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))) . x
(
((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 A39, A45, A48, FUNCT_1:47;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P2,s2,(i + 1))) . d
by A12, A30, A47, A48, A49, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A41, A47, A48, FUNCT_1:47
;
verum end;
reconsider j =
IC (Comput (P1,s1,i)) as
Element of
NAT ;
A50:
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)))
;
A51:
((IC (Comput (P1,s1,i))) + k) + 1 =
(j + k) + 1
.=
(j + 1) + k
;
not not
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 & ... & not
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8
by AMI_5:5;
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 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8 )
;
suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0
;
S1[i + 1]then A52:
CurInstr (
P1,
(Comput (P1,s1,i)))
= halt SCM
by AMI_5:7;
thus (IC (Comput (P1,s1,(i + 1)))) + k =
(IC (Comput (P1,s1,i))) + k
by A50, A52, EXTPRO_1:def 3
.=
IC (Comput (P2,s2,(i + 1)))
by A10, A36, A52, A11, 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 A31;
( (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))) )A53:
Comput (
P2,
s2,
(i + 1))
= Comput (
P2,
s2,
i)
by A36, A52, A11, EXTPRO_1:def 3;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A12, A50, A52, 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 A13, A40, A52, A53, 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 such that A54:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := db
by AMI_5:8;
A55:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= da := db
by A54, COMPOS_0:4;
A56:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A54, AMI_3:2;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A10, A11, A50, A36, A51, A55, AMI_3:2;
( 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 A10, A11, A31, A50, A36, A51, A55, A56, AMI_3:2;
( (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))) )A57:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A26;
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 A58:
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 A59:
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
x in Data-Locations
by A30, A59;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
per cases
( da = d or da <> d )
;
suppose A60:
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 A11, A50, A36, A54, A55, AMI_3:2;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A8, A30, A42, A54, A57, A59, A58, A60, A5, AMI_5:17;
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 A11, A50, A36, A54, A55, AMI_3:2;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A59;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A61:
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 by A16, AMI_2:def 16, AMI_3:27;
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 A11, A36, A40, A54, A55, AMI_3:2;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A26, A18, A61;
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 A11, A36, A40, A54, A55, AMI_3:2;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A61;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2
;
S1[i + 1]then consider da,
db being
Data-Location such that A62:
CurInstr (
P1,
(Comput (P1,s1,i)))
= AddTo (
da,
db)
by AMI_5:9;
A63:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= AddTo (
da,
db)
by A62, COMPOS_0:4;
A64:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A62, AMI_3:3;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A10, A11, A50, A36, A51, A63, AMI_3: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))) )thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A10, A11, A31, A50, A36, A51, A63, A64, AMI_3:3;
( (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))) )A65:
(
(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 A26;
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 A66:
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 A67:
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
x in Data-Locations
by A30, A67;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
per cases
( da = d or da <> d )
;
suppose A68:
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 A11, A50, A36, A62, A63, AMI_3:3;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A8, A30, A42, A62, A65, A67, A66, A68, A5, AMI_5:18;
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 A11, A50, A36, A62, A63, AMI_3:3;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A67;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A69:
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 by A16, AMI_2:def 16, AMI_3:27;
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 A11, A36, A40, A62, A63, AMI_3:3;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A18, A65, A69;
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 A11, A36, A40, A62, A63, AMI_3:3;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A69;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3
;
S1[i + 1]then consider da,
db being
Data-Location such that A70:
CurInstr (
P1,
(Comput (P1,s1,i)))
= SubFrom (
da,
db)
by AMI_5:10;
A71:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= SubFrom (
da,
db)
by A70, COMPOS_0:4;
A72:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A70, AMI_3:4;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A10, A11, A50, A36, A51, A71, AMI_3:4;
( 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 A10, A11, A31, A50, A36, A51, A71, A72, AMI_3:4;
( (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))) )A73:
(
(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 A26;
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 A74:
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 A75:
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
x in Data-Locations
by A30, A75;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
per cases
( da = d or da <> d )
;
suppose A76:
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 A11, A50, A36, A70, A71, AMI_3:4;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A8, A30, A42, A70, A73, A75, A74, A76, A5, AMI_5:19;
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 A11, A50, A36, A70, A71, AMI_3:4;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A75;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A77:
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 by A16, AMI_2:def 16, AMI_3:27;
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 A11, A36, A40, A70, A71, AMI_3:4;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A18, A73, A77;
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 A11, A36, A40, A70, A71, AMI_3:4;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A77;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4
;
S1[i + 1]then consider da,
db being
Data-Location such that A78:
CurInstr (
P1,
(Comput (P1,s1,i)))
= MultBy (
da,
db)
by AMI_5:11;
A79:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= MultBy (
da,
db)
by A78, COMPOS_0:4;
A80:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A78, AMI_3:5;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A10, A11, A50, A36, A51, A79, AMI_3:5;
( 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 A10, A11, A31, A50, A36, A51, A79, A80, AMI_3:5;
( (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))) )A81:
(
(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 A26;
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 A82:
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 A83:
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
x in Data-Locations
by A30, A83;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
per cases
( da = d or da <> d )
;
suppose A84:
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 A11, A50, A36, A78, A79, AMI_3:5;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A8, A30, A42, A78, A81, A83, A82, A84, A5, AMI_5:20;
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 A11, A50, A36, A78, A79, AMI_3:5;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A83;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A85:
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 by A16, AMI_2:def 16, AMI_3:27;
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 A11, A36, A40, A78, A79, AMI_3:5;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A18, A81, A85;
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 A11, A36, A40, A78, A79, AMI_3:5;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A85;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5
;
S1[i + 1]then consider da,
db being
Data-Location such that A86:
CurInstr (
P1,
(Comput (P1,s1,i)))
= Divide (
da,
db)
by AMI_5:12;
A87:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= Divide (
da,
db)
by A86, COMPOS_0:4;
A88:
(
(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 A26;
per cases
( da <> db or da = db )
;
suppose A89:
da <> db
;
S1[i + 1]A90:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A86, AMI_3:6;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A10, A11, A50, A36, A51, A87, AMI_3:6;
( 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 A10, A11, A31, A50, A36, A51, A87, A90, AMI_3:6;
( (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))) . x
DataPart p c= p
by RELAT_1:59;
then A91:
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 A92:
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
x in Data-Locations
by A30, A92;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
per cases
( da = d or db = d or ( da <> d & db <> d ) )
;
suppose A93:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then A94:
(
(Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) &
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
by A11, A50, A36, A86, A87, A89, AMI_3:6;
((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db)
by A1, A8, A30, A86, A89, A92, A91, A93, A5, AMI_5:21;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P2,s2,(i + 1))) . d
by A88, A92, A94, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A41, A92, FUNCT_1:47
;
verum end; suppose A95:
db = 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) mod ((Comput (P1,s1,i)) . db) &
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
by A11, A50, A36, A86, A87, AMI_3:6;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A1, A8, A30, A42, A86, A88, A92, A91, A95, A5, AMI_5:22;
verum end; suppose
(
da <> d &
db <> 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 A11, A50, A36, A86, A87, AMI_3:6;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A92;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A96:
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 by A16, AMI_2:def 16, AMI_3:27;
per cases
( da = d or db = d or ( da <> d & db <> 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) div ((Comput (P2,s2,i)) . db) &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) )
by A11, A36, A40, A86, A87, A89, AMI_3:6;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A18, A88, A96;
verum end; suppose
db = 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) mod ((Comput (P2,s2,i)) . db) &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) )
by A11, A36, A40, A86, A87, AMI_3:6;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A18, A88, A96;
verum end; suppose
(
da <> d &
db <> 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 A11, A36, A40, A86, A87, AMI_3:6;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A96;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose A97:
da = db
;
S1[i + 1]A98:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A86, AMI_3:6;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A10, A11, A50, A36, A51, A87, AMI_3:6;
( 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 A10, A11, A31, A50, A36, A51, A87, A98, AMI_3:6;
( (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 A99:
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
x in Data-Locations
by A30, A99;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
per cases
( da = d or da <> d )
;
suppose A100:
da = d
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1A101:
(
((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 A30, A39, A45, A99, FUNCT_1:47;
A102:
(
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . d = (Comput (P1,s1,(i + 1))) . d &
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . d = (Comput (P2,s2,(i + 1))) . d )
by A30, A41, A99, FUNCT_1:47;
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
by A11, A36, A87, A97, A100, AMI_3:6;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A12, A50, A86, A97, A100, A101, A102, AMI_3:6;
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 A11, A50, A36, A86, A87, A97, AMI_3:6;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A99;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A103:
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 by A16, AMI_2:def 16, AMI_3:27;
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) mod ((Comput (P2,s2,i)) . db) &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) )
by A11, A36, A40, A86, A87, A97, AMI_3:6;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A18, A88, A103;
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 A11, A36, A40, A86, A87, A97, AMI_3:6;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A103;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; end; end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6
;
S1[i + 1]then consider loc being
Nat such that A104:
CurInstr (
P1,
(Comput (P1,s1,i)))
= SCM-goto loc
by AMI_5:13;
A105:
CurInstr (
P2,
(Comput (P2,s2,i)))
= SCM-goto (loc + k)
by A11, A104, Th1;
thus (IC (Comput (P1,s1,(i + 1)))) + k =
loc + k
by A50, A104, AMI_3:7
.=
IC (Comput (P2,s2,(i + 1)))
by A36, A105, AMI_3:7
;
( 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 A31;
( (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 A106:
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
x in Data-Locations
by A30, A106;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A50, A36, A104, A105, AMI_3:7;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A106;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A107:
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 by A16, AMI_2:def 16, AMI_3:27;
(
(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 A36, A40, A104, A105, AMI_3:7;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A107;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7
;
S1[i + 1]then consider loc being
Nat,
da being
Data-Location such that A108:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da =0_goto loc
by AMI_5:14;
A109:
now ( ( (Comput (P1,s1,i)) . da = 0 & (IC (Comput (P1,s1,(i + 1)))) + k = loc + k ) or ( (Comput (P1,s1,i)) . da <> 0 & (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 ) )end; A110:
CurInstr (
P2,
(Comput (P2,s2,i)))
= da =0_goto (loc + k)
by A11, A108, Th2;
A111:
now ( ( (Comput (P2,s2,i)) . da = 0 & IC (Comput (P2,s2,(i + 1))) = loc + k ) or ( (Comput (P2,s2,i)) . da <> 0 & IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 ) )end; A112:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A26;
A113:
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, A8, A108, A112, A109, A111, A5, AMI_5:23;
verum end; end; 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)))) & (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 A31, A113;
( (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 A114:
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
x in Data-Locations
by A30, A114;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A50, A36, A108, A110, AMI_3:8;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A114;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A115:
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 by A16, AMI_2:def 16, AMI_3:27;
(
(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 A36, A40, A108, A110, AMI_3:8;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A115;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8
;
S1[i + 1]then consider loc being
Nat,
da being
Data-Location such that A116:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da >0_goto loc
by AMI_5:15;
A117:
now ( ( (Comput (P1,s1,i)) . da > 0 & (IC (Comput (P1,s1,(i + 1)))) + k = loc + k ) or ( (Comput (P1,s1,i)) . da <= 0 & (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 ) )end; A118:
CurInstr (
P2,
(Comput (P2,s2,i)))
= da >0_goto (loc + k)
by A11, A116, Th3;
A119:
now ( ( (Comput (P2,s2,i)) . da > 0 & IC (Comput (P2,s2,(i + 1))) = loc + k ) or ( (Comput (P2,s2,i)) . da <= 0 & IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 ) )end; A120:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A26;
A121:
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, A8, A116, A120, A117, A119, A5, AMI_5:24;
verum end; end; 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)))) & (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 A31, A121;
( (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 A122:
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
x in Data-Locations
by A30, A122;
then reconsider d =
x as
Data-Location by AMI_2:def 16, AMI_3:27;
(
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d &
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d )
by A50, A36, A116, A118, AMI_3:9;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A30, A46, A122;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A30, A41, 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 A123:
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 by A16, AMI_2:def 16, AMI_3:27;
(
(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 A36, A40, A116, A118, AMI_3:9;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A123;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A16, A17, GRFUNC_1:3;
verum end; end;
end;
A124:
DataPart p c= p
by RELAT_1:59;
A125:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
now ( (IC (Comput (P1,s1,0))) + k = IC (Comput (P2,s2,0)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) & (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )thus (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, A125, GRFUNC_1:2
.=
IC (Comput (P2,s2,0))
;
( IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) & (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )reconsider loc =
IC p as
Element of
NAT ;
A126:
IC p = IC s1
by A1, A3, GRFUNC_1:2;
then
IC p = IC (Comput (P1,s1,0))
;
then A127:
loc in dom q
by A7, A4, AMISTD_5:def 4;
A128:
(IC p) + k in dom (Reloc (q,k))
by A127, COMPOS_1:46;
A129:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
A130:
q . (IC p) = P1 . (IC s1)
by A126, A127, A5, GRFUNC_1:2;
dom P2 = NAT
by PARTFUN1:def 2;
then A131:
CurInstr (
P2,
(Comput (P2,s2,0))) =
P2 . (IC (Comput (P2,s2,0)))
by PARTFUN1:def 6
.=
P2 . (IC s2)
.=
P2 . (IC (IncIC (p,k)))
by A2, A129, GRFUNC_1:2
.=
P2 . ((IC p) + k)
by MEMSTR_0:53
.=
P2 . ((IC p) + k)
.=
(Reloc (q,k)) . ((IC p) + k)
by A128, A5, GRFUNC_1:2
;
A132:
dom P1 = NAT
by PARTFUN1:def 2;
CurInstr (
P1,
(Comput (P1,s1,0))) =
CurInstr (
P1,
s1)
.=
P1 . (IC s1)
by A132, PARTFUN1:def 6
;
hence
IncAddr (
(CurInstr (P1,(Comput (P1,s1,0)))),
k)
= CurInstr (
P2,
(Comput (P2,s2,0)))
by A127, A130, A131, COMPOS_1:35;
( (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )A133:
dom (DataPart s2) = Data-Locations
by MEMSTR_0:9;
A134:
DataPart p c= s1
by A1, A124, XBOOLE_1:1;
A135:
DataPart (IncIC (p,k)) = DataPart p
by MEMSTR_0:51;
DataPart p c= IncIC (
p,
k)
by A135, MEMSTR_0:12;
then A136:
DataPart p c= s2
by A2, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
.=
DataPart p
by A134, GRFUNC_1:23
.=
s2 | (dom (DataPart p))
by A136, GRFUNC_1:23
.=
(Comput (P2,s2,0)) | (dom (DataPart p))
;
DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0))thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) =
DataPart (s1 +* (DataPart s2))
.=
DataPart s2
by A133
.=
DataPart (Comput (P2,s2,0))
;
verum end;
then A137:
S1[ 0 ]
;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A137, A9); verum