let P1, P2 be Instruction-Sequence of SCMPDS; for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let p be non empty q -autonomic FinPartState of SCMPDS; for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let s1, s2 be State of SCMPDS; ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) )
assume that
A1:
( p c= s1 & p c= s2 )
and
A2:
( q c= P1 & q c= P2 )
; for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
A3:
( p c= s1 & p c= s2 )
by A1;
let i be Nat; for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let k1, k2 be Integer; for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let a, b be Int_position; ( CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
assume that
A4:
CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2)
and
A5:
a in dom p
and
A6:
DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p
; ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
( a in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . a = (Comput (P1,s1,i)) . a & ((Comput (P2,s2,i)) | (dom p)) . a = (Comput (P2,s2,i)) . a ) )
by FUNCT_1:49;
then A7:
(Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a
by A5, A2, A3, EXTPRO_1:def 10;
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set D11 = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1));
set D21 = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1));
Comput (P1,s1,(i + 1)) =
Following (P1,(Comput (P1,s1,i)))
by EXTPRO_1:3
.=
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))
;
then A8:
(Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)))
by A4, SCMPDS_2:51;
A9: Comput (P2,s2,(i + 1)) =
Following (P2,(Comput (P2,s2,i)))
by EXTPRO_1:3
.=
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i)))
;
A10:
( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) )
by FUNCT_1:49;
CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i)))
by A1, A2, AMISTD_5:7;
then
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
by A9, A4, SCMPDS_2:51;
hence
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
by A10, A6, A7, A8, A2, A3, EXTPRO_1:def 10; verum