let k be Element of NAT ; for p being autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st IC SCM+FSA in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
let p be autonomic FinPartState of SCM+FSA ; for s1, s2 being State of SCM+FSA st IC SCM+FSA in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
let s1, s2 be State of SCM+FSA ; ( IC SCM+FSA in dom p & p c= s1 & Relocated p,k c= s2 implies for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
assume that
A1:
IC SCM+FSA in dom p
and
A2:
p c= s1
and
A3:
Relocated p,k c= s2
; for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
set s3 = s1 +* (DataPart s2);
defpred S1[ Nat] means ( (IC (Comput (ProgramPart s1),s1,$1)) + k = IC (Comput (ProgramPart s2),s2,$1) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,$1)),(Comput (ProgramPart s1),s1,$1)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,$1)),(Comput (ProgramPart s2),s2,$1) & (Comput (ProgramPart s1),s1,$1) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,$1) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),$1) = DataPart (Comput (ProgramPart s2),s2,$1) );
A4:
not p is NAT -defined
by A1, AMI_1:109;
A5:
p c= s1 +* (DataPart s2)
by A2, A3, Th10;
A6:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set DPp =
DataPart p;
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume that A7:
(IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i)
and A8:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i)
and A9:
(Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k)))
and A10:
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i)
;
S1[i + 1]
set Cs1i1 =
Comput (ProgramPart s1),
s1,
(i + 1);
set Cs1i =
Comput (ProgramPart s1),
s1,
i;
A11:
dom (Comput (ProgramPart s1),s1,(i + 1)) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT
by PARTFUN1:def 4, SCMFSA_2:8;
set Cs3i =
Comput (ProgramPart (s1 +* (DataPart s2))),
(s1 +* (DataPart s2)),
i;
set Cs2i =
Comput (ProgramPart s2),
s2,
i;
A12:
dom (Comput (ProgramPart s1),s1,i) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT
by PARTFUN1:def 4, SCMFSA_2:8;
set Cs2i1 =
Comput (ProgramPart s2),
s2,
(i + 1);
A13:
dom (Comput (ProgramPart s2),s2,(i + 1)) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT
by PARTFUN1:def 4, SCMFSA_2:8;
A14:
dom (Comput (ProgramPart s2),s2,i) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT
by PARTFUN1:def 4, SCMFSA_2:8;
set I =
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i);
T:
ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,i)
by AMI_1:144;
A15:
Comput (ProgramPart s2),
s2,
(i + 1) =
Following (ProgramPart s2),
(Comput (ProgramPart s2),s2,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i)
by T
;
A17:
now let d be
FinSeq-Location ;
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d = (Comput (ProgramPart s2),s2,i) . dA18:
d in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i))
by A16;
hence (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d =
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)) . d
by FUNCT_1:70
.=
(Comput (ProgramPart s2),s2,i) . d
by A10, A18, FUNCT_1:70
;
verum end;
set Cs3i1 =
Comput (ProgramPart (s1 +* (DataPart s2))),
(s1 +* (DataPart s2)),
(i + 1);
A19:
dom (DataPart (Comput (ProgramPart s2),s2,i)) = Int-Locations \/ FinSeq-Locations
by SCMFSA_2:127, SCMNORM:14;
A20:
dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) = Int-Locations \/ FinSeq-Locations
by SCMFSA_2:127, SCMNORM:14;
A21:
now reconsider loc =
IC (Comput (ProgramPart s1),s1,(i + 1)) as
Element of
NAT ;
assume A22:
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
;
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1))reconsider ii =
loc as
Element of
NAT ;
A23:
ii in dom (ProgramPart p)
by A2, A4, SCMFSA_3:17;
ProgramPart p c= p
by RELAT_1:88;
then A24:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then
loc + k in dom (Relocated p,k)
by A23, Th4;
then A25:
(Relocated p,k) . (loc + k) =
s2 . (loc + k)
by A3, GRFUNC_1:8
.=
(Comput (ProgramPart s2),s2,(i + 1)) . (loc + k)
by AMI_1:54
;
Z:
(ProgramPart (Comput (ProgramPart s2),s2,(i + 1))) /. (IC (Comput (ProgramPart s2),s2,(i + 1))) = (Comput (ProgramPart s2),s2,(i + 1)) . (IC (Comput (ProgramPart s2),s2,(i + 1)))
by AMI_1:150;
(ProgramPart (Comput (ProgramPart s1),s1,(i + 1))) /. (IC (Comput (ProgramPart s1),s1,(i + 1))) = (Comput (ProgramPart s1),s1,(i + 1)) . (IC (Comput (ProgramPart s1),s1,(i + 1)))
by AMI_1:150;
then CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),
(Comput (ProgramPart s1),s1,(i + 1)) =
s1 . loc
by AMI_1:54
.=
p . ii
by A2, A23, A24, GRFUNC_1:8
;
hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A22, A23, A25, Th7, Z;
verum end;
A27:
now let d be
Int-Location ;
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d = (Comput (ProgramPart s2),s2,i) . dA28:
d in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i))
by A26;
hence (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d =
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)) . d
by FUNCT_1:70
.=
(Comput (ProgramPart s2),s2,i) . d
by A10, A28, FUNCT_1:70
;
verum end;
dom (DataPart p) = (dom p) /\ (Int-Locations \/ FinSeq-Locations )
by RELAT_1:90, SCMFSA_2:127;
then A29:
dom (DataPart p) c= {(IC SCM+FSA )} \/ (Int-Locations \/ FinSeq-Locations )
by XBOOLE_1:10, XBOOLE_1:17;
A30:
( not
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) <= 9
+ 1 or
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) <= 8
+ 1 or
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 10 )
by NAT_1:8;
A31:
( not
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) <= 10
+ 1 or
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) <= 10 or
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 11 )
by NAT_1:8;
A32:
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) <= 11
+ 1
by SCMFSA_2:35;
A33:
dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) =
(dom (Comput (ProgramPart s1),s1,(i + 1))) /\ (dom (DataPart p))
by RELAT_1:90
.=
dom (DataPart p)
by A11, A29, XBOOLE_1:10, XBOOLE_1:28
;
A34:
dom (DataPart (Comput (ProgramPart s2),s2,(i + 1))) = Int-Locations \/ FinSeq-Locations
by SCMFSA_2:127, SCMNORM:14;
A35:
now let x be
set ;
( x in dom ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) | (Int-Locations \/ FinSeq-Locations )) & (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume that A36:
x in dom ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) | (Int-Locations \/ FinSeq-Locations ))
and A37:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthus (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . x
by A36, A37, FUNCT_1:70, SCMFSA_2:127
.=
(DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A20, A34, A36, FUNCT_1:70, SCMFSA_2:127
;
verum end;
A38:
dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)) = Int-Locations \/ FinSeq-Locations
by SCMFSA_2:127, SCMNORM:14;
A39:
now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) & (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . x & (Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume that A40:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
and A41:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . x
and A42:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)) . x = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . x
by A38, A20, A40, FUNCT_1:70;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A10, A19, A20, A35, A40, A41, A42, FUNCT_1:70, SCMFSA_2:127;
verum end;
T:
ProgramPart (s1 +* (DataPart s2)) = ProgramPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)
by AMI_1:144;
A43:
Comput (ProgramPart (s1 +* (DataPart s2))),
(s1 +* (DataPart s2)),
(i + 1) =
Following (ProgramPart (s1 +* (DataPart s2))),
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i)
by A2, A4, A5, SCMFSA_3:18, T
;
A44:
dom (DataPart p) = dom (DataPart (Relocated p,k))
by Th1;
then A45:
dom ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))) =
(dom (Comput (ProgramPart s2),s2,(i + 1))) /\ (dom (DataPart p))
by RELAT_1:90
.=
dom (DataPart p)
by A13, A29, XBOOLE_1:10, XBOOLE_1:28
;
A46:
now let x,
d be
set ;
( d = x & d in dom (DataPart p) & (Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s2),s2,(i + 1)) . d implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume that A47:
d = x
and A48:
d in dom (DataPart p)
and A49:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s2),s2,(i + 1)) . d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . xthus ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . d
by A33, A47, A48, A49, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A45, A47, A48, FUNCT_1:70
;
verum end;
A50:
dom ((Comput (ProgramPart s1),s1,i) | (dom (DataPart p))) =
(dom (Comput (ProgramPart s1),s1,i)) /\ (dom (DataPart p))
by RELAT_1:90
.=
dom (DataPart p)
by A12, A29, XBOOLE_1:10, XBOOLE_1:28
;
reconsider j =
IC (Comput (ProgramPart s1),s1,i) as
Element of
NAT ;
T:
ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,i)
by AMI_1:144;
A51:
Comput (ProgramPart s1),
s1,
(i + 1) =
Following (ProgramPart s1),
(Comput (ProgramPart s1),s1,i)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i)
by T
;
A52:
dom ((Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k)))) =
(dom (Comput (ProgramPart s2),s2,i)) /\ (dom (DataPart p))
by A44, RELAT_1:90
.=
dom (DataPart p)
by A14, A29, XBOOLE_1:10, XBOOLE_1:28
;
A53:
now let x,
d be
set ;
( d = x & d in dom (DataPart p) & (Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d & (Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume that A54:
d = x
and A55:
d in dom (DataPart p)
and A56:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
and A57:
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . xA58:
((Comput (ProgramPart s1),s1,i) | (dom (DataPart p))) . d = (Comput (ProgramPart s1),s1,i) . d
by A50, A55, FUNCT_1:70;
((Comput (ProgramPart s2),s2,i) | (dom (DataPart p))) . d = (Comput (ProgramPart s2),s2,i) . d
by A44, A52, A55, FUNCT_1:70;
hence ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . d
by A9, A44, A33, A54, A55, A56, A57, A58, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A45, A54, A55, FUNCT_1:70
;
verum end;
A59:
succ ((IC (Comput (ProgramPart s1),s1,i)) + k) =
(j + k) + 1
by NAT_1:39
.=
(j + 1) + k
.=
(succ (IC (Comput (ProgramPart s1),s1,i))) + k
by NAT_1:39
;
per cases
( InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 0 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 1 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 2 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 3 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 4 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 5 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 6 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 7 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 8 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 9 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 10 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 11 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 12 )
by A32, A31, A30, NAT_1:8, NAT_1:33;
suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 0
;
S1[i + 1]then A60:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = halt SCM+FSA
by SCMFSA_2:122;
then A61:
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) = halt SCM+FSA
by A8, SCMFSA_4:8;
thus (IC (Comput (ProgramPart s1),s1,(i + 1))) + k =
(IC (Comput (ProgramPart s1),s1,i)) + k
by A51, A60, AMI_1:def 8
.=
IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A15, A61, AMI_1:def 8
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A21;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A62:
Comput (ProgramPart s2),
s2,
(i + 1) = Comput (ProgramPart s2),
s2,
i
by A15, A61, AMI_1:def 8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A9, A51, A60, AMI_1:def 8;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))thus
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A10, A43, A60, A62, AMI_1:def 8;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 1
;
S1[i + 1]then consider da,
db being
Int-Location such that A63:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da := db
by SCMFSA_2:54;
A64:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = da := db
by A63, SCMFSA_4:9;
A65:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A63, SCMFSA_2:89;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A64, SCMFSA_2:89;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A64, A65, SCMFSA_2:89;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A66:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )A67:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
assume A68:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A68, A67, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A69:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A63, SCMFSA_2:89;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A64, SCMFSA_2:89;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A68, A69;
verum end; suppose A70:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then
dom (DataPart p) c= dom p
by GRFUNC_1:8;
then A71:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s1),s1,i) . db
by A2, A4, A5, A33, A63, A68, A70, SCMFSA_3:19;
A72:
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s1),s1,i) . db
by A51, A63, A70, SCMFSA_2:89;
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . db
by A8, A15, A64, A70, SCMFSA_2:89;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A66, A68, A72, A71;
verum end; suppose A73:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A74:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A63, A73, SCMFSA_2:89;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A64, A73, SCMFSA_2:89;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A68, A74;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A75:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A75, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider f =
x as
FinSeq-Location by SCMFSA_2:12;
A76:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . f = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f
by A43, A63, SCMFSA_2:89;
(Comput (ProgramPart s2),s2,(i + 1)) . f = (Comput (ProgramPart s2),s2,i) . f
by A8, A15, A64, SCMFSA_2:89;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A75, A76;
verum end; suppose A77:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1A78:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . da = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db
by A43, A63, SCMFSA_2:89;
(Comput (ProgramPart s2),s2,(i + 1)) . da = (Comput (ProgramPart s2),s2,i) . db
by A8, A15, A64, SCMFSA_2:89;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A27, A35, A75, A77, A78, SCMFSA_2:127;
verum end; suppose A79:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A80:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A63, A79, SCMFSA_2:89;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A64, A79, SCMFSA_2:89;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A75, A80;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 2
;
S1[i + 1]then consider da,
db being
Int-Location such that A81:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = AddTo da,
db
by SCMFSA_2:55;
A82:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
A83:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = AddTo da,
db
by A81, SCMFSA_4:10;
A84:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A81, SCMFSA_2:90;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A83, SCMFSA_2:90;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A83, A84, SCMFSA_2:90;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A85:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
now A86:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A87:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A87, A86, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A88:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A81, SCMFSA_2:90;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A83, SCMFSA_2:90;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A87, A88;
verum end; suppose A89:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then A90:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
A91:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . da) + ((Comput (ProgramPart s1),s1,i) . db)
by A51, A81, A89, SCMFSA_2:90;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) + ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A83, A89, SCMFSA_2:90;
then
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
by A2, A4, A5, A33, A81, A85, A82, A87, A89, A91, A90, SCMFSA_3:20;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A87;
verum end; suppose A92:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A93:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A81, A92, SCMFSA_2:90;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A83, A92, SCMFSA_2:90;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A87, A93;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A94:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A94, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A95:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A81, SCMFSA_2:90;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A83, SCMFSA_2:90;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A94, A95;
verum end; suppose A96:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A97:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) + ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db)
by A43, A81, SCMFSA_2:90;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) + ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A83, A96, SCMFSA_2:90;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A85, A82, A94, A97, SCMFSA_2:127;
verum end; suppose A98:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A99:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A81, A98, SCMFSA_2:90;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A83, A98, SCMFSA_2:90;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A94, A99;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 3
;
S1[i + 1]then consider da,
db being
Int-Location such that A100:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = SubFrom da,
db
by SCMFSA_2:56;
A101:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
A102:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = SubFrom da,
db
by A100, SCMFSA_4:11;
A103:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A100, SCMFSA_2:91;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A102, SCMFSA_2:91;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A102, A103, SCMFSA_2:91;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A104:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
now A105:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A106:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A106, A105, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A107:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A100, SCMFSA_2:91;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A102, SCMFSA_2:91;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A106, A107;
verum end; suppose A108:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then A109:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
A110:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . da) - ((Comput (ProgramPart s1),s1,i) . db)
by A51, A100, A108, SCMFSA_2:91;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) - ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A102, A108, SCMFSA_2:91;
then
((Comput (ProgramPart s1),s1,i) . da) - ((Comput (ProgramPart s1),s1,i) . db) = (Comput (ProgramPart s2),s2,(i + 1)) . x
by A2, A4, A5, A33, A100, A104, A101, A106, A108, A109, SCMFSA_3:21;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A106, A110;
verum end; suppose A111:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A112:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A100, A111, SCMFSA_2:91;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A102, A111, SCMFSA_2:91;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A106, A112;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A113:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A113, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A114:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A100, SCMFSA_2:91;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A102, SCMFSA_2:91;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A113, A114;
verum end; suppose A115:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A116:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) - ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db)
by A43, A100, SCMFSA_2:91;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) - ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A102, A115, SCMFSA_2:91;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A104, A101, A113, A116, SCMFSA_2:127;
verum end; suppose A117:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A118:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A100, A117, SCMFSA_2:91;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A102, A117, SCMFSA_2:91;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A113, A118;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 4
;
S1[i + 1]then consider da,
db being
Int-Location such that A119:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = MultBy da,
db
by SCMFSA_2:57;
A120:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
A121:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = MultBy da,
db
by A119, SCMFSA_4:12;
A122:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A119, SCMFSA_2:92;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A121, SCMFSA_2:92;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A121, A122, SCMFSA_2:92;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A123:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
now A124:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A125:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A125, A124, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A126:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A119, SCMFSA_2:92;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A121, SCMFSA_2:92;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A125, A126;
verum end; suppose A127:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then A128:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
A129:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . da) * ((Comput (ProgramPart s1),s1,i) . db)
by A51, A119, A127, SCMFSA_2:92;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) * ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A121, A127, SCMFSA_2:92;
then
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
by A2, A4, A5, A33, A119, A123, A120, A125, A127, A129, A128, SCMFSA_3:22;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A125;
verum end; suppose A130:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A131:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A119, A130, SCMFSA_2:92;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A121, A130, SCMFSA_2:92;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A125, A131;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A132:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A132, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A133:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A119, SCMFSA_2:92;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A121, SCMFSA_2:92;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A132, A133;
verum end; suppose A134:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A135:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) * ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db)
by A43, A119, SCMFSA_2:92;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) * ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A121, A134, SCMFSA_2:92;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A123, A120, A132, A135, SCMFSA_2:127;
verum end; suppose A136:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A137:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A119, A136, SCMFSA_2:92;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A121, A136, SCMFSA_2:92;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A132, A137;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 5
;
S1[i + 1]then consider da,
db being
Int-Location such that A138:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = Divide da,
db
by SCMFSA_2:58;
A139:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
A140:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = Divide da,
db
by A138, SCMFSA_4:13;
A141:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
now per cases
( da <> db or da = db )
;
suppose A142:
da <> db
;
( (IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1)) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A143:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A138, SCMFSA_2:93;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A140, SCMFSA_2:93;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A140, A143, SCMFSA_2:93;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now A144:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A145:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( ( db <> x & x in FinSeq-Locations ) or da = x or db = x or ( da <> x & db <> x & x in Int-Locations ) )
by A33, A145, A144, XBOOLE_0:def 3;
suppose
(
db <> x &
x in FinSeq-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A146:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A138, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, SCMFSA_2:93;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A145, A146;
verum end; suppose A147:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then
dom (DataPart p) c= dom p
by GRFUNC_1:8;
then A148:
((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) div ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db) = ((Comput (ProgramPart s1),s1,i) . da) div ((Comput (ProgramPart s1),s1,i) . db)
by A2, A4, A5, A33, A138, A142, A145, A147, SCMFSA_3:23;
A149:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . da) div ((Comput (ProgramPart s1),s1,i) . db)
by A51, A138, A142, A147, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) div ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A140, A142, A147, SCMFSA_2:93;
hence ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x =
(Comput (ProgramPart s2),s2,(i + 1)) . x
by A141, A139, A145, A149, A148, FUNCT_1:70
.=
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A44, A33, A45, A145, FUNCT_1:70
;
verum end; suppose A150:
db = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then A151:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
A152:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . da) mod ((Comput (ProgramPart s1),s1,i) . db)
by A51, A138, A150, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A140, A150, SCMFSA_2:93;
then
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
by A2, A4, A5, A33, A138, A141, A139, A145, A150, A152, A151, SCMFSA_3:24;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A145;
verum end; suppose A153:
(
da <> x &
db <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A154:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A138, A153, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, A153, SCMFSA_2:93;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A145, A154;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A155:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),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 A20, A155, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A156:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A138, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, SCMFSA_2:93;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A155, A156;
verum end; suppose A157:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A158:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) div ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db)
by A43, A138, A142, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) div ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A140, A142, A157, SCMFSA_2:93;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A141, A139, A155, A158, SCMFSA_2:127;
verum end; suppose A159:
db = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A160:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) mod ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db)
by A43, A138, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A140, A159, SCMFSA_2:93;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A141, A139, A155, A160, SCMFSA_2:127;
verum end; suppose A161:
(
da <> x &
db <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A162:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A138, A161, SCMFSA_2:93;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, A161, SCMFSA_2:93;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A155, A162;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose A163:
da = db
;
( (IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1)) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )then A164:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A138, SCMFSA_2:94;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A140, A163, SCMFSA_2:94;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A140, A163, A164, SCMFSA_2:94;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now A165:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )assume A166:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A166, A165, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A167:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A138, A163, SCMFSA_2:94;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, A163, SCMFSA_2:94;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A166, A167;
verum end; suppose A168:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1A169:
((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x = (Comput (ProgramPart s2),s2,(i + 1)) . x
by A44, A33, A45, A166, FUNCT_1:70;
A170:
((Comput (ProgramPart s1),s1,i) | (dom (DataPart p))) . x = (Comput (ProgramPart s1),s1,i) . x
by A33, A50, A166, FUNCT_1:70;
A171:
((Comput (ProgramPart s2),s2,i) | (dom (DataPart p))) . x = (Comput (ProgramPart s2),s2,i) . x
by A44, A33, A52, A166, FUNCT_1:70;
A172:
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = (Comput (ProgramPart s1),s1,(i + 1)) . x
by A166, FUNCT_1:70;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A140, A163, A168, SCMFSA_2:94;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A9, A44, A51, A138, A163, A168, A170, A171, A172, A169, SCMFSA_2:94;
verum end; suppose A173:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A174:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A138, A163, A173, SCMFSA_2:94;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, A163, A173, SCMFSA_2:94;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A166, A174;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A175:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A175, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A176:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A138, A163, SCMFSA_2:94;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, A163, SCMFSA_2:94;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A175, A176;
verum end; suppose A177:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A178:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) mod ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db)
by A43, A138, A163, SCMFSA_2:94;
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db)
by A8, A15, A140, A163, A177, SCMFSA_2:94;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A141, A139, A175, A178, SCMFSA_2:127;
verum end; suppose A179:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A180:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A138, A163, A179, SCMFSA_2:94;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A140, A163, A179, SCMFSA_2:94;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A175, A180;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; hence
S1[
i + 1]
;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 6
;
S1[i + 1]then consider loc being
Element of
NAT such that A181:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = goto loc
by SCMFSA_2:59;
A182:
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) = goto (loc + k)
by A8, A181, SCMFSA_4:14;
thus (IC (Comput (ProgramPart s1),s1,(i + 1))) + k =
loc + k
by A51, A181, SCMFSA_2:95
.=
IC (Comput (ProgramPart s2),s2,(i + 1))
by A15, A182, SCMFSA_2:95
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A21;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume A183:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
then
(
x in Int-Locations or
x in FinSeq-Locations )
by A33, A183, XBOOLE_0:def 3;
then A184:
(
x is
Int-Location or
x is
FinSeq-Location )
by SCMFSA_2:11, SCMFSA_2:12;
then A185:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
by A15, A182, SCMFSA_2:95;
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s1),s1,i) . x
by A51, A181, A184, SCMFSA_2:95;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A183, A185;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A186:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen
(
x in Int-Locations or
x in FinSeq-Locations )
by A20, XBOOLE_0:def 3;
then A187:
(
x is
Int-Location or
x is
FinSeq-Location )
by SCMFSA_2:11, SCMFSA_2:12;
then A188:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
by A15, A182, SCMFSA_2:95;
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . x
by A43, A181, A187, SCMFSA_2:95;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A186, A188;
verum end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 7
;
S1[i + 1]then consider loc being
Element of
NAT ,
da being
Int-Location such that A189:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da =0_goto loc
by SCMFSA_2:60;
A191:
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) = da =0_goto (loc + k)
by A8, A189, SCMFSA_4:15;
A193:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
A194:
now per cases
( loc <> succ (IC (Comput (ProgramPart s1),s1,i)) or loc = succ (IC (Comput (ProgramPart s1),s1,i)) )
;
suppose
loc <> succ (IC (Comput (ProgramPart s1),s1,i))
;
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A2, A4, A5, A189, A193, A190, A192, SCMFSA_3:25;
verum end; hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A21, A194;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume A195:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
then
(
x in Int-Locations or
x in FinSeq-Locations )
by A33, A195, XBOOLE_0:def 3;
then A196:
(
x is
Int-Location or
x is
FinSeq-Location )
by SCMFSA_2:11, SCMFSA_2:12;
then A197:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
by A15, A191, SCMFSA_2:96;
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s1),s1,i) . x
by A51, A189, A196, SCMFSA_2:96;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A195, A197;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A198:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen
(
x in Int-Locations or
x in FinSeq-Locations )
by A20, XBOOLE_0:def 3;
then A199:
(
x is
Int-Location or
x is
FinSeq-Location )
by SCMFSA_2:11, SCMFSA_2:12;
then A200:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
by A15, A191, SCMFSA_2:96;
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . x
by A43, A189, A199, SCMFSA_2:96;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A198, A200;
verum end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 8
;
S1[i + 1]then consider loc being
Element of
NAT ,
da being
Int-Location such that A201:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da >0_goto loc
by SCMFSA_2:61;
A203:
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) = da >0_goto (loc + k)
by A8, A201, SCMFSA_4:16;
A205:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
A206:
now per cases
( loc <> succ (IC (Comput (ProgramPart s1),s1,i)) or loc = succ (IC (Comput (ProgramPart s1),s1,i)) )
;
suppose
loc <> succ (IC (Comput (ProgramPart s1),s1,i))
;
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A2, A4, A5, A201, A205, A202, A204, SCMFSA_3:26;
verum end; hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A21, A206;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x )assume A207:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
then
(
x in Int-Locations or
x in FinSeq-Locations )
by A33, A207, XBOOLE_0:def 3;
then A208:
(
x is
Int-Location or
x is
FinSeq-Location )
by SCMFSA_2:11, SCMFSA_2:12;
then A209:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
by A15, A203, SCMFSA_2:97;
(Comput (ProgramPart s1),s1,(i + 1)) . x = (Comput (ProgramPart s1),s1,i) . x
by A51, A201, A208, SCMFSA_2:97;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A207, A209;
verum end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x )assume A210:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . xthen
(
x in Int-Locations or
x in FinSeq-Locations )
by A20, XBOOLE_0:def 3;
then A211:
(
x is
Int-Location or
x is
FinSeq-Location )
by SCMFSA_2:11, SCMFSA_2:12;
then A212:
(Comput (ProgramPart s2),s2,(i + 1)) . x = (Comput (ProgramPart s2),s2,i) . x
by A15, A203, SCMFSA_2:97;
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . x
by A43, A201, A211, SCMFSA_2:97;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A210, A212;
verum end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 9
;
S1[i + 1]then consider db,
da being
Int-Location ,
f being
FinSeq-Location such that A213:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da := f,
db
by SCMFSA_2:62;
A214:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f = (Comput (ProgramPart s2),s2,i) . f
by A17;
A215:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = da := f,
db
by A213, SCMFSA_4:17;
A216:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A213, SCMFSA_2:98;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A215, SCMFSA_2:98;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A215, A216, SCMFSA_2:98;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A217:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )A218:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
assume A219:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A219, A218, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A220:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A213, SCMFSA_2:98;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A215, SCMFSA_2:98;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A219, A220;
verum end; suppose A221:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then consider k1 being
Element of
NAT such that A222:
k1 = abs ((Comput (ProgramPart s1),s1,i) . db)
and A223:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . f) /. k1
by A51, A213, SCMFSA_2:98;
consider k2 being
Element of
NAT such that A224:
k2 = abs ((Comput (ProgramPart s2),s2,i) . db)
and A225:
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . f) /. k2
by A8, A15, A215, A221, SCMFSA_2:98;
DataPart p c= p
by RELAT_1:88;
then
dom (DataPart p) c= dom p
by GRFUNC_1:8;
then
((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f) /. k2 = ((Comput (ProgramPart s1),s1,i) . f) /. k1
by A2, A4, A5, A33, A213, A217, A219, A221, A222, A224, SCMFSA_3:27;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A214, A219, A223, A225;
verum end; suppose A226:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A227:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A213, A226, SCMFSA_2:98;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A215, A226, SCMFSA_2:98;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A219, A227;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A228:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A228, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider f =
x as
FinSeq-Location by SCMFSA_2:12;
A229:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . f = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f
by A43, A213, SCMFSA_2:98;
(Comput (ProgramPart s2),s2,(i + 1)) . f = (Comput (ProgramPart s2),s2,i) . f
by A8, A15, A215, SCMFSA_2:98;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A228, A229;
verum end; suppose A230:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A231:
ex
k1 being
Element of
NAT st
(
k1 = abs ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db) &
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f) /. k1 )
by A43, A213, SCMFSA_2:98;
ex
k2 being
Element of
NAT st
(
k2 = abs ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . f) /. k2 )
by A8, A15, A215, A230, SCMFSA_2:98;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A217, A214, A228, A231, SCMFSA_2:127;
verum end; suppose A232:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A233:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A213, A232, SCMFSA_2:98;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A215, A232, SCMFSA_2:98;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A228, A233;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 10
;
S1[i + 1]then consider db,
da being
Int-Location ,
f being
FinSeq-Location such that A234:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = f,
db := da
by SCMFSA_2:63;
A235:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f = (Comput (ProgramPart s2),s2,i) . f
by A17;
A236:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = f,
db := da
by A234, SCMFSA_4:18;
A237:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A234, SCMFSA_2:99;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A236, SCMFSA_2:99;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A238:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A236, A237, SCMFSA_2:99;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A239:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db = (Comput (ProgramPart s2),s2,i) . db
by A27;
now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )A240:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
assume A241:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A33, A241, A240, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A242:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A234, SCMFSA_2:99;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A236, SCMFSA_2:99;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A241, A242;
verum end; suppose A243:
f = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then consider k1 being
Element of
NAT such that A244:
k1 = abs ((Comput (ProgramPart s1),s1,i) . db)
and A245:
(Comput (ProgramPart s1),s1,(i + 1)) . x = ((Comput (ProgramPart s1),s1,i) . f) +* k1,
((Comput (ProgramPart s1),s1,i) . da)
by A51, A234, SCMFSA_2:99;
consider k2 being
Element of
NAT such that A246:
k2 = abs ((Comput (ProgramPart s2),s2,i) . db)
and A247:
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . f) +* k2,
((Comput (ProgramPart s2),s2,i) . da)
by A8, A15, A236, A243, SCMFSA_2:99;
DataPart p c= p
by RELAT_1:88;
then
dom (DataPart p) c= dom p
by GRFUNC_1:8;
then
((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f) +* k2,
((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) = ((Comput (ProgramPart s1),s1,i) . f) +* k1,
((Comput (ProgramPart s1),s1,i) . da)
by A2, A4, A5, A33, A234, A239, A241, A243, A244, A246, SCMFSA_3:28;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A238, A235, A241, A245, A247;
verum end; suppose A248:
(
f <> x &
x in FinSeq-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A249:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A234, A248, SCMFSA_2:99;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A236, A248, SCMFSA_2:99;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A241, A249;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A250:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A20, A250, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider f =
x as
Int-Location by SCMFSA_2:11;
A251:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . f = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f
by A43, A234, SCMFSA_2:99;
(Comput (ProgramPart s2),s2,(i + 1)) . f = (Comput (ProgramPart s2),s2,i) . f
by A8, A15, A236, SCMFSA_2:99;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A250, A251;
verum end; suppose A252:
f = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A253:
ex
k1 being
Element of
NAT st
(
k1 = abs ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . db) &
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f) +* k1,
((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) )
by A43, A234, SCMFSA_2:99;
ex
k2 being
Element of
NAT st
(
k2 = abs ((Comput (ProgramPart s2),s2,i) . db) &
(Comput (ProgramPart s2),s2,(i + 1)) . x = ((Comput (ProgramPart s2),s2,i) . f) +* k2,
((Comput (ProgramPart s2),s2,i) . da) )
by A8, A15, A236, A252, SCMFSA_2:99;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A239, A238, A235, A250, A253, SCMFSA_2:127;
verum end; suppose A254:
(
f <> x &
x in FinSeq-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A255:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A234, A254, SCMFSA_2:99;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A236, A254, SCMFSA_2:99;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A250, A255;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 11
;
S1[i + 1]then consider da being
Int-Location ,
f being
FinSeq-Location such that A256:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da :=len f
by SCMFSA_2:64;
A257:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = da :=len f
by A256, SCMFSA_4:19;
A258:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A256, SCMFSA_2:100;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A257, SCMFSA_2:100;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A257, A258, SCMFSA_2:100;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A259:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f = (Comput (ProgramPart s2),s2,i) . f
by A17;
now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )A260:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
assume A261:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A33, A261, A260, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A262:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A256, SCMFSA_2:100;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A257, SCMFSA_2:100;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A261, A262;
verum end; suppose A263:
da = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1
DataPart p c= p
by RELAT_1:88;
then
dom (DataPart p) c= dom p
by GRFUNC_1:8;
then A264:
len ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f) = len ((Comput (ProgramPart s1),s1,i) . f)
by A2, A4, A5, A33, A256, A261, A263, SCMFSA_3:29;
A265:
(Comput (ProgramPart s1),s1,(i + 1)) . x = len ((Comput (ProgramPart s1),s1,i) . f)
by A51, A256, A263, SCMFSA_2:100;
(Comput (ProgramPart s2),s2,(i + 1)) . x = len ((Comput (ProgramPart s2),s2,i) . f)
by A8, A15, A257, A263, SCMFSA_2:100;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A259, A261, A265, A264;
verum end; suppose A266:
(
da <> x &
x in Int-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A267:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A256, A266, SCMFSA_2:100;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A257, A266, SCMFSA_2:100;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A261, A267;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A268:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) )
by A20, A268, XBOOLE_0:def 3;
suppose
x in FinSeq-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider f =
x as
FinSeq-Location by SCMFSA_2:12;
A269:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . f = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f
by A43, A256, SCMFSA_2:100;
(Comput (ProgramPart s2),s2,(i + 1)) . f = (Comput (ProgramPart s2),s2,i) . f
by A8, A15, A257, SCMFSA_2:100;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A268, A269;
verum end; suppose A270:
da = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A271:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = len ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f)
by A43, A256, SCMFSA_2:100;
(Comput (ProgramPart s2),s2,(i + 1)) . x = len ((Comput (ProgramPart s2),s2,i) . f)
by A8, A15, A257, A270, SCMFSA_2:100;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A259, A268, A271, SCMFSA_2:127;
verum end; suppose A272:
(
da <> x &
x in Int-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A273:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A256, A272, SCMFSA_2:100;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A257, A272, SCMFSA_2:100;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A268, A273;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end; suppose
InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) = 12
;
S1[i + 1]then consider da being
Int-Location ,
f being
FinSeq-Location such that A274:
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = f :=<0,...,0> da
by SCMFSA_2:65;
A275:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = f :=<0,...,0> da
by A274, SCMFSA_4:20;
A276:
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,i))
by A274, SCMFSA_2:101;
hence
(IC (Comput (ProgramPart s1),s1,(i + 1))) + k = IC (Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A51, A15, A59, A275, SCMFSA_2:101;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),(Comput (ProgramPart s2),s2,(i + 1)) & (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )thus
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(i + 1))),(Comput (ProgramPart s1),s1,(i + 1))),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(i + 1))),
(Comput (ProgramPart s2),s2,(i + 1))
by A7, A8, A21, A51, A15, A59, A275, A276, SCMFSA_2:101;
( (Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1)) )A277:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da = (Comput (ProgramPart s2),s2,i) . da
by A27;
now let x be
set ;
( x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) implies ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1 )A278:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
assume A279:
x in dom ((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)))
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A33, A279, A278, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
Int-Location by SCMFSA_2:11;
A280:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A274, SCMFSA_2:101;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A275, SCMFSA_2:101;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A279, A280;
verum end; suppose A281:
f = x
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then consider k1 being
Element of
NAT such that A282:
k1 = abs ((Comput (ProgramPart s1),s1,i) . da)
and A283:
(Comput (ProgramPart s1),s1,(i + 1)) . x = k1 |-> 0
by A51, A274, SCMFSA_2:101;
consider k2 being
Element of
NAT such that A284:
k2 = abs ((Comput (ProgramPart s2),s2,i) . da)
and A285:
(Comput (ProgramPart s2),s2,(i + 1)) . x = k2 |-> 0
by A8, A15, A275, A281, SCMFSA_2:101;
DataPart p c= p
by RELAT_1:88;
then
dom (DataPart p) c= dom p
by GRFUNC_1:8;
then
k2 |-> 0 = k1 |-> 0
by A2, A4, A5, A33, A274, A277, A279, A281, A282, A284, SCMFSA_3:30;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A46, A279, A283, A285;
verum end; suppose A286:
(
f <> x &
x in FinSeq-Locations )
;
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . b1 = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A287:
(Comput (ProgramPart s1),s1,(i + 1)) . d = (Comput (ProgramPart s1),s1,i) . d
by A51, A274, A286, SCMFSA_2:101;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A275, A286, SCMFSA_2:101;
hence
((Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p))) . x = ((Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))) . x
by A33, A53, A279, A287;
verum end; end; then
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) c= (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart p))
by A44, A33, A45, GRFUNC_1:8;
hence
(Comput (ProgramPart s1),s1,(i + 1)) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,(i + 1)) | (dom (DataPart (Relocated p,k)))
by A44, A33, A45, GRFUNC_1:9;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))now let x be
set ;
( x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) implies (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1 )assume A288:
x in dom (DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)))
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1per cases
( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) )
by A20, A288, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider f =
x as
Int-Location by SCMFSA_2:11;
A289:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . f = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . f
by A43, A274, SCMFSA_2:101;
(Comput (ProgramPart s2),s2,(i + 1)) . f = (Comput (ProgramPart s2),s2,i) . f
by A8, A15, A275, SCMFSA_2:101;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A288, A289;
verum end; suppose A290:
f = x
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then A291:
ex
k1 being
Element of
NAT st
(
k1 = abs ((Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . da) &
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . x = k1 |-> 0 )
by A43, A274, SCMFSA_2:101;
ex
k2 being
Element of
NAT st
(
k2 = abs ((Comput (ProgramPart s2),s2,i) . da) &
(Comput (ProgramPart s2),s2,(i + 1)) . x = k2 |-> 0 )
by A8, A15, A275, A290, SCMFSA_2:101;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A35, A277, A288, A291, SCMFSA_2:127;
verum end; suppose A292:
(
f <> x &
x in FinSeq-Locations )
;
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . b1 = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . b1then reconsider d =
x as
FinSeq-Location by SCMFSA_2:12;
A293:
(Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) . d = (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) . d
by A43, A274, A292, SCMFSA_2:101;
(Comput (ProgramPart s2),s2,(i + 1)) . d = (Comput (ProgramPart s2),s2,i) . d
by A8, A15, A275, A292, SCMFSA_2:101;
hence
(DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Comput (ProgramPart s2),s2,(i + 1))) . x
by A39, A288, A293;
verum end; end; then
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) c= DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:8;
hence
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),(i + 1)) = DataPart (Comput (ProgramPart s2),s2,(i + 1))
by A20, A34, GRFUNC_1:9;
verum end;
end;
A294:
DataPart p = DataPart (Relocated p,k)
by Th1;
reconsider ii = IC p as Element of NAT ;
A295:
DataPart p c= p
by RELAT_1:88;
A296:
DataPart (Relocated p,k) c= Relocated p,k
by RELAT_1:88;
A297:
IC SCM+FSA in dom (Relocated p,k)
by Th5;
now thus (IC (Comput (ProgramPart s1),s1,0 )) + k =
(IC s1) + k
by AMI_1:13
.=
(IC p) + k
by A1, A2, GRFUNC_1:8
.=
IC (Relocated p,k)
by Th6
.=
IC s2
by A3, A297, GRFUNC_1:8
.=
IC (Comput (ProgramPart s2),s2,0 )
by AMI_1:13
;
( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,0 )),(Comput (ProgramPart s1),s1,0 )),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,0 )),(Comput (ProgramPart s2),s2,0 ) & (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),0 ) = DataPart (Comput (ProgramPart s2),s2,0 ) )reconsider loc =
IC p as
Element of
NAT ;
Z:
(ProgramPart s1) /. (IC s1) = s1 . (IC s1)
by AMI_1:150;
V:
Comput (ProgramPart s1),
s1,
0 = s1
by AMI_1:13;
A298:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,0 )),(Comput (ProgramPart s1),s1,0 )),
k =
IncAddr (CurInstr (ProgramPart s1),s1),
k
by V
.=
IncAddr (s1 . (IC s1)),
k
by Z
;
A299:
IC p = IC s1
by A1, A2, GRFUNC_1:8;
then
IC p = IC (Comput (ProgramPart s1),s1,0 )
by AMI_1:13;
then A300:
loc in dom (ProgramPart p)
by A2, A4, SCMFSA_3:17;
ProgramPart p c= p
by RELAT_1:88;
then A301:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then A302:
(IC p) + k in dom (Relocated p,k)
by A300, Th4;
A303:
IC SCM+FSA in dom (Relocated p,k)
by Th5;
A304:
p . ii = s1 . (IC s1)
by A2, A299, A300, A301, GRFUNC_1:8;
V:
Comput (ProgramPart s2),
s2,
0 = s2
by AMI_1:13;
Z:
(ProgramPart s2) /. (IC s2) = s2 . (IC s2)
by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,0 )),
(Comput (ProgramPart s2),s2,0 ) =
CurInstr (ProgramPart s2),
s2
by V
.=
s2 . (IC (Relocated p,k))
by A3, A303, GRFUNC_1:8, Z
.=
s2 . ((IC p) + k)
by Th6
.=
(Relocated p,k) . ((IC p) + k)
by A3, A302, GRFUNC_1:8
;
hence
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,0 )),(Comput (ProgramPart s1),s1,0 )),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,0 )),
(Comput (ProgramPart s2),s2,0 )
by A300, A304, A298, Th7;
( (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),0 ) = DataPart (Comput (ProgramPart s2),s2,0 ) )thus (Comput (ProgramPart s1),s1,0 ) | (dom (DataPart p)) =
s1 | (dom (DataPart p))
by AMI_1:13
.=
DataPart p
by A2, A295, GRFUNC_1:64, XBOOLE_1:1
.=
s2 | (dom (DataPart p))
by A3, A294, A296, GRFUNC_1:64, XBOOLE_1:1
.=
(Comput (ProgramPart s2),s2,0 ) | (dom (DataPart (Relocated p,k)))
by A294, AMI_1:13
;
DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),0 ) = DataPart (Comput (ProgramPart s2),s2,0 )thus DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),0 ) =
DataPart (s1 +* (DataPart s2))
by AMI_1:13
.=
DataPart s2
by PBOOLE:157
.=
DataPart (Comput (ProgramPart s2),s2,0 )
by AMI_1:13
;
verum end;
then A305:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A305, A6); verum