let k be Nat; for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA 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+FSA -valued finite non halt-free Function; for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA 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+FSA; for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA 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+FSA; ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA 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+FSA 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+FSA; ( 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)) )
A5:
Reloc (q,k) c= P2
by A4;
A6:
q c= P1
by A4;
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)) );
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 Cs1i1 =
Comput (
P1,
s1,
(i + 1));
set Cs1i =
Comput (
P1,
s1,
i);
A13:
dom (Comput (P1,s1,(i + 1))) = (Data-Locations ) \/ {(IC )}
by MEMSTR_0:13;
set Cs3i =
Comput (
P1,
(s1 +* (DataPart s2)),
i);
set Cs2i =
Comput (
P2,
s2,
i);
A14:
dom (Comput (P1,s1,i)) = (Data-Locations ) \/ {(IC )}
by MEMSTR_0:13;
set Cs2i1 =
Comput (
P2,
s2,
(i + 1));
A15:
dom (Comput (P2,s2,(i + 1))) = (Data-Locations ) \/ {(IC )}
by MEMSTR_0:13;
A16:
dom (Comput (P2,s2,i)) = (Data-Locations ) \/ {(IC )}
by MEMSTR_0:13;
set I =
CurInstr (
P1,
(Comput (P1,s1,i)));
A17:
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)))
;
A19:
now for d being FinSeq-Location holds (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dlet d be
FinSeq-Location ;
(Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dA20:
d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i)))
by A18;
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, A20, FUNCT_1:47
;
verum end;
set Cs3i1 =
Comput (
P1,
(s1 +* (DataPart s2)),
(i + 1));
A21:
dom (DataPart (Comput (P2,s2,i))) = Data-Locations
by MEMSTR_0:9;
A22:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations
by MEMSTR_0:9;
A23:
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
Nat ;
assume A24:
(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 ii =
loc as
Nat ;
A25:
ii in dom q
by A6, A1, AMISTD_5:def 4;
A26:
loc + k in dom (Reloc (q,k))
by A25, COMPOS_1:46;
A27:
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 A25, A4, GRFUNC_1:2
.=
q . loc
;
hence IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k) =
(Reloc (q,k)) . (loc + k)
by A25, COMPOS_1:35
.=
P2 . (IC (Comput (P2,s2,(i + 1))))
by A24, A26, A5, GRFUNC_1:2
.=
CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A27, PARTFUN1:def 6
;
verum end;
A29:
now for d being Int-Location holds (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dlet d be
Int-Location;
(Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . dA30:
d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i)))
by A28;
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, A30, FUNCT_1:47
;
verum end;
dom (DataPart p) = (dom p) /\ (Data-Locations )
by RELAT_1:61;
then A31:
dom (DataPart p) c= {(IC )} \/ (Data-Locations )
by XBOOLE_1:10, XBOOLE_1:17;
A32:
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 A13, A31, XBOOLE_1:28
;
A33:
dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations
by MEMSTR_0:9;
A34:
now for x being object st x in dom ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations )) & (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
object ;
( x in dom ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations )) & (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 A35:
x in dom ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations ))
and A36:
(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 A35, A36, FUNCT_1:47
.=
(DataPart (Comput (P2,s2,(i + 1)))) . x
by A22, A33, A35, FUNCT_1:47
;
verum end;
A37:
dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations
by MEMSTR_0:9;
A38:
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 A39:
x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))))
and A40:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x
and A41:
(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 A37, A22, A39, FUNCT_1:47;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A12, A21, A22, A34, A39, A40, A41, FUNCT_1:47;
verum end;
A42:
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
;
A43:
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 A15, A31, XBOOLE_1:28
;
A44:
now for x, d being set 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,
d be
set ;
( 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 A45:
d = x
and A46:
d in dom (DataPart p)
and A47:
(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 A32, A45, A46, A47, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A43, A45, A46, FUNCT_1:47
;
verum end;
A48:
dom ((Comput (P1,s1,i)) | (dom (DataPart p))) =
(dom (Comput (P1,s1,i))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A14, A31, XBOOLE_1:28
;
reconsider j =
IC (Comput (P1,s1,i)) as
Nat ;
A49:
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)))
;
A50:
dom ((Comput (P2,s2,i)) | (dom (DataPart p))) =
(dom (Comput (P2,s2,i))) /\ (dom (DataPart p))
by RELAT_1:61
.=
dom (DataPart p)
by A16, A31, XBOOLE_1:28
;
A51:
now for x, d being set 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,
d be
set ;
( 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 A52:
d = x
and A53:
d in dom (DataPart p)
and A54:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
and A55:
(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))) . xA56:
((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d
by A48, A53, FUNCT_1:47;
((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d
by A50, A53, FUNCT_1:47;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P2,s2,(i + 1))) . d
by A11, A32, A52, A53, A54, A55, A56, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A43, A52, A53, FUNCT_1:47
;
verum end;
A57:
((IC (Comput (P1,s1,i))) + k) + 1 =
(j + k) + 1
.=
(j + 1) + k
.=
((IC (Comput (P1,s1,i))) + 1) + k
;
not not
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 & ... & not
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12
by SCMFSA_2:16;
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 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 9 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 10 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 11 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12 )
;
suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0
;
S1[i + 1]then A58:
CurInstr (
P1,
(Comput (P1,s1,i)))
= halt SCM+FSA
by SCMFSA_2:95;
thus (IC (Comput (P1,s1,(i + 1)))) + k =
(IC (Comput (P1,s1,i))) + k
by A49, A58, EXTPRO_1:def 3
.=
IC (Comput (P2,s2,(i + 1)))
by A9, A17, A58, A10, 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 A23;
( (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 (
P2,
s2,
(i + 1))
= Comput (
P2,
s2,
i)
by A17, A58, A10, EXTPRO_1:def 3;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A11, A49, A58, 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, A42, A58, A59, EXTPRO_1:def 3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1
;
S1[i + 1]then consider da,
db being
Int-Location such that A60:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := db
by SCMFSA_2:30;
A61:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= da := db
by A60, COMPOS_0:4;
A62:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A60, SCMFSA_2:63;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A61, SCMFSA_2:63;
( 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, A23, A49, A17, A57, A61, A62, SCMFSA_2:63;
( (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))) )A63:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
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 )A64:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
assume A65:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A65, A64, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A66:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A60, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A61, SCMFSA_2:63;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A65, A66;
verum end; suppose A67:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then
dom (DataPart p) c= dom p
by GRFUNC_1:2;
then A68:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P1,s1,i)) . db
by A1, A7, A32, A60, A65, A67, A4, SCMFSA_3:5;
A69:
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . db
by A49, A60, A67, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . db
by A10, A17, A61, A67, SCMFSA_2:63;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A63, A65, A69, A68;
verum end; suppose A70:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A71:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A60, A70, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A61, A70, SCMFSA_2:63;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A65, A71;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A72:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A72, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider f =
x as
FinSeq-Location by SCMFSA_2:def 5;
A73:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f
by A42, A60, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f
by A10, A17, A61, SCMFSA_2:63;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A72, A73;
verum end; suppose A74:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1A75:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . da = (Comput (P1,(s1 +* (DataPart s2)),i)) . db
by A42, A60, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db
by A10, A17, A61, SCMFSA_2:63;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A29, A34, A72, A74, A75;
verum end; suppose A76:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A77:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A60, A76, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A61, A76, SCMFSA_2:63;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A72, A77;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2
;
S1[i + 1]then consider da,
db being
Int-Location such that A78:
CurInstr (
P1,
(Comput (P1,s1,i)))
= AddTo (
da,
db)
by SCMFSA_2:31;
A79:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
A80:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= AddTo (
da,
db)
by A78, COMPOS_0:4;
A81:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A78, SCMFSA_2:64;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A80, SCMFSA_2:64;
( 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, A23, A49, A17, A57, A80, A81, SCMFSA_2:64;
( (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))) )A82:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
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))) . xA83:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
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 A84:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A84, A83, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A85:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A78, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A80, SCMFSA_2:64;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A84, A85;
verum end; suppose A86:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then A87:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
A88:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db)
by A49, A78, A86, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
by A10, A17, A80, A86, SCMFSA_2:64;
then
(Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x
by A1, A7, A32, A78, A82, A79, A84, A86, A88, A87, A4, SCMFSA_3:6;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A84;
verum end; suppose A89:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A90:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A78, A89, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A80, A89, SCMFSA_2:64;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A84, A90;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A91:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A91, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A92:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A78, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A80, SCMFSA_2:64;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A91, A92;
verum end; suppose A93:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A94:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db)
by A42, A78, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
by A10, A17, A80, A93, SCMFSA_2:64;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A82, A79, A91, A94;
verum end; suppose A95:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A96:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A78, A95, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A80, A95, SCMFSA_2:64;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A91, A96;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3
;
S1[i + 1]then consider da,
db being
Int-Location such that A97:
CurInstr (
P1,
(Comput (P1,s1,i)))
= SubFrom (
da,
db)
by SCMFSA_2:32;
A98:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
A99:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= SubFrom (
da,
db)
by A97, COMPOS_0:4;
A100:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A97, SCMFSA_2:65;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A99, SCMFSA_2:65;
( 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, A23, A49, A17, A57, A99, A100, SCMFSA_2:65;
( (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))) )A101:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
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))) . xA102:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
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 A103:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A103, A102, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A104:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A97, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A99, SCMFSA_2:65;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A103, A104;
verum end; suppose A105:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then A106:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
A107:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db)
by A49, A97, A105, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
by A10, A17, A99, A105, SCMFSA_2:65;
then
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = (Comput (P2,s2,(i + 1))) . x
by A1, A7, A32, A97, A101, A98, A103, A105, A106, A4, SCMFSA_3:7;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A103, A107;
verum end; suppose A108:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A109:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A97, A108, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A99, A108, SCMFSA_2:65;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A103, A109;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A110:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A110, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A111:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A97, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A99, SCMFSA_2:65;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A110, A111;
verum end; suppose A112:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A113:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db)
by A42, A97, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
by A10, A17, A99, A112, SCMFSA_2:65;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A101, A98, A110, A113;
verum end; suppose A114:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A115:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A97, A114, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A99, A114, SCMFSA_2:65;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A110, A115;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4
;
S1[i + 1]then consider da,
db being
Int-Location such that A116:
CurInstr (
P1,
(Comput (P1,s1,i)))
= MultBy (
da,
db)
by SCMFSA_2:33;
A117:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
A118:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= MultBy (
da,
db)
by A116, COMPOS_0:4;
A119:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A116, SCMFSA_2:66;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A118, SCMFSA_2:66;
( 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, A23, A49, A17, A57, A118, A119, SCMFSA_2:66;
( (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))) )A120:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
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))) . xA121:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
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 A122:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A122, A121, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A123:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A116, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A118, SCMFSA_2:66;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A122, A123;
verum end; suppose A124:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then A125:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
A126:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db)
by A49, A116, A124, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
by A10, A17, A118, A124, SCMFSA_2:66;
then
(Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x
by A1, A7, A32, A116, A120, A117, A122, A124, A126, A125, A4, SCMFSA_3:8;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A122;
verum end; suppose A127:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A128:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A116, A127, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A118, A127, SCMFSA_2:66;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A122, A128;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A129:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A129, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A130:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A116, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A118, SCMFSA_2:66;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A129, A130;
verum end; suppose A131:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A132:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db)
by A42, A116, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
by A10, A17, A118, A131, SCMFSA_2:66;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A120, A117, A129, A132;
verum end; suppose A133:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A134:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A116, A133, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A118, A133, SCMFSA_2:66;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A129, A134;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5
;
S1[i + 1]then consider da,
db being
Int-Location such that A135:
CurInstr (
P1,
(Comput (P1,s1,i)))
= Divide (
da,
db)
by SCMFSA_2:34;
A136:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
A137:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= Divide (
da,
db)
by A135, COMPOS_0:4;
A138:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
per cases
( da <> db or da = db )
;
suppose A139:
da <> db
;
S1[i + 1]A140:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A135, SCMFSA_2:67;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A137, SCMFSA_2:67;
( 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, A23, A49, A17, A57, A137, A140, SCMFSA_2:67;
( (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))) . xA141:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
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 A142:
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))) . b1per cases
( ( db <> x & x in FinSeq-Locations ) or da = x or db = x or ( da <> x & db <> x & x in Int-Locations ) )
by A32, A142, A141, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
(
db <> x &
x in FinSeq-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A143:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A135, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, SCMFSA_2:67;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A142, A143;
verum end; suppose A144:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then
dom (DataPart p) c= dom p
by GRFUNC_1:2;
then A145:
((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, A7, A32, A135, A139, A142, A144, A4, SCMFSA_3:9;
A146:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db)
by A49, A135, A139, A144, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
by A10, A17, A137, A139, A144, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x =
(Comput (P2,s2,(i + 1))) . x
by A138, A136, A142, A146, A145, FUNCT_1:47
.=
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A43, A142, FUNCT_1:47
;
verum end; suppose A147:
db = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then A148:
dom (DataPart p) c= dom p
by GRFUNC_1:2;
A149:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db)
by A49, A135, A147, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
by A10, A17, A137, A147, SCMFSA_2:67;
then
(Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x
by A1, A7, A32, A135, A138, A136, A142, A147, A149, A148, A4, SCMFSA_3:10;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A142;
verum end; suppose A150:
(
da <> x &
db <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A151:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A135, A150, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, A150, SCMFSA_2:67;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A142, A151;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A152:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or db = x or ( da <> x & db <> x & x in Int-Locations ) )
by A22, A152, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A153:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A135, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, SCMFSA_2:67;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A152, A153;
verum end; suppose A154:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A155:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db)
by A42, A135, A139, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
by A10, A17, A137, A139, A154, SCMFSA_2:67;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A138, A136, A152, A155;
verum end; suppose A156:
db = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A157:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db)
by A42, A135, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
by A10, A17, A137, A156, SCMFSA_2:67;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A138, A136, A152, A157;
verum end; suppose A158:
(
da <> x &
db <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A159:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A135, A158, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, A158, SCMFSA_2:67;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A152, A159;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose A160:
da = db
;
S1[i + 1]then A161:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A135, SCMFSA_2:68;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A137, A160, SCMFSA_2:68;
( 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, A23, A49, A17, A57, A137, A160, A161, SCMFSA_2:68;
( (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))) . xA162:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
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 A163:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A163, A162, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A164:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A135, A160, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, A160, SCMFSA_2:68;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A163, A164;
verum end; suppose A165:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1A166:
((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x
by A32, A43, A163, FUNCT_1:47;
A167:
((Comput (P1,s1,i)) | (dom (DataPart p))) . x = (Comput (P1,s1,i)) . x
by A32, A48, A163, FUNCT_1:47;
A168:
((Comput (P2,s2,i)) | (dom (DataPart p))) . x = (Comput (P2,s2,i)) . x
by A32, A50, A163, FUNCT_1:47;
A169:
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . x
by A163, FUNCT_1:47;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
by A10, A17, A137, A160, A165, SCMFSA_2:68;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A11, A49, A135, A160, A165, A167, A168, A169, A166, SCMFSA_2:68;
verum end; suppose A170:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A171:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A135, A160, A170, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, A160, A170, SCMFSA_2:68;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A163, A171;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A172:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A172, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A173:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A135, A160, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, A160, SCMFSA_2:68;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A172, A173;
verum end; suppose A174:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A175:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db)
by A42, A135, A160, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
by A10, A17, A137, A160, A174, SCMFSA_2:68;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A138, A136, A172, A175;
verum end; suppose A176:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A177:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A135, A160, A176, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A137, A160, A176, SCMFSA_2:68;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A172, A177;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, 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 A178:
CurInstr (
P1,
(Comput (P1,s1,i)))
= goto loc
by SCMFSA_2:35;
A179:
CurInstr (
P2,
(Comput (P2,s2,i)))
= goto (loc + k)
by A10, A178, SCMFSA_4:1;
thus (IC (Comput (P1,s1,(i + 1)))) + k =
loc + k
by A49, A178, SCMFSA_2:69
.=
IC (Comput (P2,s2,(i + 1)))
by A17, A179, SCMFSA_2:69
;
( 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 A23;
( (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 A180:
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 Int-Locations or
x in FinSeq-Locations )
by A32, A180, SCMFSA_2:100, XBOOLE_0:def 3;
then A181:
(
x is
Int-Location or
x is
FinSeq-Location )
by AMI_2:def 16, SCMFSA_2:def 5;
then A182:
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x
by A17, A179, SCMFSA_2:69;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x
by A49, A178, A181, SCMFSA_2:69;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A180, A182;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A183:
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
(
x in Int-Locations or
x in FinSeq-Locations )
by A22, SCMFSA_2:100, XBOOLE_0:def 3;
then A184:
(
x is
Int-Location or
x is
FinSeq-Location )
by AMI_2:def 16, SCMFSA_2:def 5;
then A185:
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x
by A17, A179, SCMFSA_2:69;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x
by A42, A178, A184, SCMFSA_2:69;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A183, A185;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7
;
S1[i + 1]then consider loc being
Nat,
da being
Int-Location such that A186:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da =0_goto loc
by SCMFSA_2:36;
A187:
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; A188:
CurInstr (
P2,
(Comput (P2,s2,i)))
= da =0_goto (loc + k)
by A10, A186, SCMFSA_4:2;
A189:
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; A190:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
A191:
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, A186, A190, A187, A189, A4, SCMFSA_3:11;
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 A23, A191;
( (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 A192:
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 Int-Locations or
x in FinSeq-Locations )
by A32, A192, SCMFSA_2:100, XBOOLE_0:def 3;
then A193:
(
x is
Int-Location or
x is
FinSeq-Location )
by AMI_2:def 16, SCMFSA_2:def 5;
then A194:
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x
by A17, A188, SCMFSA_2:70;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x
by A49, A186, A193, SCMFSA_2:70;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A192, A194;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A195:
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
(
x in Int-Locations or
x in FinSeq-Locations )
by A22, SCMFSA_2:100, XBOOLE_0:def 3;
then A196:
(
x is
Int-Location or
x is
FinSeq-Location )
by AMI_2:def 16, SCMFSA_2:def 5;
then A197:
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x
by A17, A188, SCMFSA_2:70;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x
by A42, A186, A196, SCMFSA_2:70;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A195, A197;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8
;
S1[i + 1]then consider loc being
Nat,
da being
Int-Location such that A198:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da >0_goto loc
by SCMFSA_2:37;
A199:
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; A200:
CurInstr (
P2,
(Comput (P2,s2,i)))
= da >0_goto (loc + k)
by A10, A198, SCMFSA_4:3;
A201:
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; A202:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
A203:
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, A198, A202, A199, A201, A4, SCMFSA_3:12;
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 A23, A203;
( (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 A204:
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 Int-Locations or
x in FinSeq-Locations )
by A32, A204, SCMFSA_2:100, XBOOLE_0:def 3;
then A205:
(
x is
Int-Location or
x is
FinSeq-Location )
by AMI_2:def 16, SCMFSA_2:def 5;
then A206:
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x
by A17, A200, SCMFSA_2:71;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x
by A49, A198, A205, SCMFSA_2:71;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A204, A206;
verum end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A207:
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
(
x in Int-Locations or
x in FinSeq-Locations )
by A22, SCMFSA_2:100, XBOOLE_0:def 3;
then A208:
(
x is
Int-Location or
x is
FinSeq-Location )
by AMI_2:def 16, SCMFSA_2:def 5;
then A209:
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x
by A17, A200, SCMFSA_2:71;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x
by A42, A198, A208, SCMFSA_2:71;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A207, A209;
verum end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 9
;
S1[i + 1]then consider db,
da being
Int-Location,
f being
FinSeq-Location such that A210:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := (
f,
db)
by SCMFSA_2:38;
A211:
(Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f
by A19;
A212:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= da := (
f,
db)
by A210, COMPOS_0:4;
A213:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A210, SCMFSA_2:72;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A212, SCMFSA_2:72;
( 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, A23, A49, A17, A57, A212, A213, SCMFSA_2:72;
( (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))) )A214:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
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 )A215:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
assume A216:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A216, A215, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A217:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A210, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A212, SCMFSA_2:72;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A216, A217;
verum end; suppose A218:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then consider k1 being
Nat such that A219:
k1 = |.((Comput (P1,s1,i)) . db).|
and A220:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) /. k1
by A49, A210, SCMFSA_2:72;
consider k2 being
Nat such that A221:
k2 = |.((Comput (P2,s2,i)) . db).|
and A222:
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2
by A10, A17, A212, A218, SCMFSA_2:72;
DataPart p c= p
by RELAT_1:59;
then
dom (DataPart p) c= dom p
by GRFUNC_1:2;
then
((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k2 = ((Comput (P1,s1,i)) . f) /. k1
by A1, A7, A32, A210, A214, A216, A218, A219, A221, A4, SCMFSA_3:13;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A211, A216, A220, A222;
verum end; suppose A223:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A224:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A210, A223, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A212, A223, SCMFSA_2:72;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A216, A224;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A225:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A225, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider f =
x as
FinSeq-Location by SCMFSA_2:def 5;
A226:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f
by A42, A210, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f
by A10, A17, A212, SCMFSA_2:72;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A225, A226;
verum end; suppose A227:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A228:
ex
k1 being
Nat st
(
k1 = |.((Comput (P1,(s1 +* (DataPart s2)),i)) . db).| &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k1 )
by A42, A210, SCMFSA_2:72;
ex
k2 being
Nat st
(
k2 = |.((Comput (P2,s2,i)) . db).| &
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 )
by A10, A17, A212, A227, SCMFSA_2:72;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A214, A211, A225, A228;
verum end; suppose A229:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A230:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A210, A229, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A212, A229, SCMFSA_2:72;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A225, A230;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 10
;
S1[i + 1]then consider db,
da being
Int-Location,
f being
FinSeq-Location such that A231:
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
f,
db)
:= da
by SCMFSA_2:39;
A232:
(Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f
by A19;
A233:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= (
f,
db)
:= da
by A231, COMPOS_0:4;
A234:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A231, SCMFSA_2:73;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A233, SCMFSA_2:73;
( 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))) )A235:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
thus
IncAddr (
(CurInstr (P1,(Comput (P1,s1,(i + 1))))),
k)
= CurInstr (
P2,
(Comput (P2,s2,(i + 1))))
by A9, A10, A23, A49, A17, A57, A233, A234, SCMFSA_2:73;
( (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))) )A236:
(Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db
by A29;
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 )A237:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
assume A238:
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))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A32, A238, A237, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A239:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A231, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A233, SCMFSA_2:73;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A238, A239;
verum end; suppose A240:
f = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then consider k1 being
Nat such that A241:
k1 = |.((Comput (P1,s1,i)) . db).|
and A242:
(Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) +* (
k1,
((Comput (P1,s1,i)) . da))
by A49, A231, SCMFSA_2:73;
consider k2 being
Nat such that A243:
k2 = |.((Comput (P2,s2,i)) . db).|
and A244:
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (
k2,
((Comput (P2,s2,i)) . da))
by A10, A17, A233, A240, SCMFSA_2:73;
DataPart p c= p
by RELAT_1:59;
then
dom (DataPart p) c= dom p
by GRFUNC_1:2;
then
((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (
k2,
((Comput (P1,(s1 +* (DataPart s2)),i)) . da))
= ((Comput (P1,s1,i)) . f) +* (
k1,
((Comput (P1,s1,i)) . da))
by A1, A7, A32, A231, A236, A238, A240, A241, A243, A4, SCMFSA_3:14;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A235, A232, A238, A242, A244;
verum end; suppose A245:
(
f <> x &
x in FinSeq-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A246:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A231, A245, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A233, A245, SCMFSA_2:73;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A238, A246;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A247:
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)))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A22, A247, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider f =
x as
Int-Location by AMI_2:def 16;
A248:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f
by A42, A231, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f
by A10, A17, A233, SCMFSA_2:73;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A247, A248;
verum end; suppose A249:
f = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A250:
ex
k1 being
Nat st
(
k1 = |.((Comput (P1,(s1 +* (DataPart s2)),i)) . db).| &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (
k1,
((Comput (P1,(s1 +* (DataPart s2)),i)) . da)) )
by A42, A231, SCMFSA_2:73;
ex
k2 being
Nat st
(
k2 = |.((Comput (P2,s2,i)) . db).| &
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (
k2,
((Comput (P2,s2,i)) . da)) )
by A10, A17, A233, A249, SCMFSA_2:73;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A236, A235, A232, A247, A250;
verum end; suppose A251:
(
f <> x &
x in FinSeq-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A252:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A231, A251, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A233, A251, SCMFSA_2:73;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A247, A252;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 11
;
S1[i + 1]then consider da being
Int-Location,
f being
FinSeq-Location such that A253:
CurInstr (
P1,
(Comput (P1,s1,i)))
= da :=len f
by SCMFSA_2:40;
A254:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= da :=len f
by A253, COMPOS_0:4;
A255:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A253, SCMFSA_2:74;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A254, SCMFSA_2:74;
( 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, A23, A49, A17, A57, A254, A255, SCMFSA_2:74;
( (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))) )A256:
(Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f
by A19;
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 )A257:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
assume A258:
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))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A32, A258, A257, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A259:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A253, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A254, SCMFSA_2:74;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A258, A259;
verum end; suppose A260:
da = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:59;
then
dom (DataPart p) c= dom p
by GRFUNC_1:2;
then A261:
len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) = len ((Comput (P1,s1,i)) . f)
by A1, A7, A32, A253, A258, A260, A4, SCMFSA_3:15;
A262:
(Comput (P1,s1,(i + 1))) . x = len ((Comput (P1,s1,i)) . f)
by A49, A253, A260, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f)
by A10, A17, A254, A260, SCMFSA_2:74;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A256, A258, A262, A261;
verum end; suppose A263:
(
da <> x &
x in Int-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A264:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A253, A263, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A254, A263, SCMFSA_2:74;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A258, A264;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A265:
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)))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A22, A265, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider f =
x as
FinSeq-Location by SCMFSA_2:def 5;
A266:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f
by A42, A253, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f
by A10, A17, A254, SCMFSA_2:74;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A265, A266;
verum end; suppose A267:
da = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A268:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f)
by A42, A253, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f)
by A10, A17, A254, A267, SCMFSA_2:74;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A256, A265, A268;
verum end; suppose A269:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A270:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A253, A269, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A254, A269, SCMFSA_2:74;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A265, A270;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; suppose
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12
;
S1[i + 1]then consider da being
Int-Location,
f being
FinSeq-Location such that A271:
CurInstr (
P1,
(Comput (P1,s1,i)))
= f :=<0,...,0> da
by SCMFSA_2:41;
A272:
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= f :=<0,...,0> da
by A271, COMPOS_0:4;
A273:
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1
by A271, SCMFSA_2:75;
hence
(IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
by A9, A10, A49, A17, A57, A272, SCMFSA_2:75;
( 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, A23, A49, A17, A57, A272, A273, SCMFSA_2:75;
( (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))) )A274:
(Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da
by A29;
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 )A275:
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
assume A276:
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))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A32, A276, A275, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by AMI_2:def 16;
A277:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A271, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A272, SCMFSA_2:75;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A276, A277;
verum end; suppose A278:
f = x
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then consider k1 being
Nat such that A279:
k1 = |.((Comput (P1,s1,i)) . da).|
and A280:
(Comput (P1,s1,(i + 1))) . x = k1 |-> 0
by A49, A271, SCMFSA_2:75;
consider k2 being
Nat such that A281:
k2 = |.((Comput (P2,s2,i)) . da).|
and A282:
(Comput (P2,s2,(i + 1))) . x = k2 |-> 0
by A10, A17, A272, A278, SCMFSA_2:75;
DataPart p c= p
by RELAT_1:59;
then
dom (DataPart p) c= dom p
by GRFUNC_1:2;
then
k2 |-> 0 = k1 |-> 0
by A1, A7, A32, A271, A274, A276, A278, A279, A281, A4, SCMFSA_3:16;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A44, A276, A280, A282;
verum end; suppose A283:
(
f <> x &
x in FinSeq-Locations )
;
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A284:
(Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d
by A49, A271, A283, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A272, A283, SCMFSA_2:75;
hence
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
by A32, A51, A276, A284;
verum end; end; end; then
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, GRFUNC_1:2;
hence
(Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p))
by A32, A43, 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 A285:
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)))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A22, A285, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider f =
x as
Int-Location by AMI_2:def 16;
A286:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f
by A42, A271, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f
by A10, A17, A272, SCMFSA_2:75;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A285, A286;
verum end; suppose A287:
f = x
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then A288:
ex
k1 being
Nat st
(
k1 = |.((Comput (P1,(s1 +* (DataPart s2)),i)) . da).| &
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = k1 |-> 0 )
by A42, A271, SCMFSA_2:75;
ex
k2 being
Nat st
(
k2 = |.((Comput (P2,s2,i)) . da).| &
(Comput (P2,s2,(i + 1))) . x = k2 |-> 0 )
by A10, A17, A272, A287, SCMFSA_2:75;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A34, A274, A285, A288;
verum end; suppose A289:
(
f <> x &
x in FinSeq-Locations )
;
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:def 5;
A290:
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d
by A42, A271, A289, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d
by A10, A17, A272, A289, SCMFSA_2:75;
hence
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
by A38, A285, A290;
verum end; end; end; then
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:2;
hence
DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
by A22, A33, GRFUNC_1:3;
verum end; end;
end;
reconsider ii = IC p as Nat ;
A291:
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, A291, 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
Nat ;
A292:
IC p = IC s1
by A1, A3, GRFUNC_1:2;
then
IC p = IC (Comput (P1,s1,0))
;
then A293:
loc in dom q
by A6, A1, AMISTD_5:def 4;
A294:
(IC p) + k in dom (Reloc (q,k))
by A293, COMPOS_1:46;
A295:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
A296:
q . (IC p) = P1 . (IC s1)
by A292, A293, A4, GRFUNC_1:2;
dom P2 = NAT
by PARTFUN1:def 2;
then A297:
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, A295, GRFUNC_1:2
.=
P2 . ((IC p) + k)
by MEMSTR_0:53
.=
P2 . ((IC p) + k)
.=
(Reloc (q,k)) . ((IC p) + k)
by A294, A4, GRFUNC_1:2
;
A298:
dom P1 = NAT
by PARTFUN1:def 2;
CurInstr (
P1,
(Comput (P1,s1,0))) =
CurInstr (
P1,
s1)
.=
P1 . (IC s1)
by A298, PARTFUN1:def 6
;
hence
IncAddr (
(CurInstr (P1,(Comput (P1,s1,0)))),
k)
= CurInstr (
P2,
(Comput (P2,s2,0)))
by A297, A293, A296, 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)) )A299:
DataPart p c= p
by RELAT_1:59;
A300:
DataPart p c= s1
by A1, A299, XBOOLE_1:1;
A301:
DataPart (IncIC (p,k)) = DataPart p
by MEMSTR_0:51;
DataPart p c= IncIC (
p,
k)
by A301, MEMSTR_0:12;
then A302:
DataPart p c= s2
by A2, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
.=
DataPart p
by A300, GRFUNC_1:23
.=
s2 | (dom (DataPart p))
by A302, 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 PBOOLE:142
.=
DataPart (Comput (P2,s2,0))
;
verum end;
then A303:
S1[ 0 ]
;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A303, A8); verum