let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for q being NAT -defined the Instructions of SCMPDS -valued finite non halt-free Function
for p being non empty b₁ -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 Element of 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 Instructions of SCMPDS -valued finite non halt-free Function; :: thesis: 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 Element of 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; :: thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of 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; :: thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i being Element of 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 ) ; :: thesis: for i being Element of 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)))
B1: ( p c= s1 & p c= s2 ) by A1;
let i be Element of NAT ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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
A3: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) and
A4: a in dom p and
A5: DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p ; :: thesis: ((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 A6: (Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a by A4, A2, B1, 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 A7: (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 A3, SCMPDS_2:51;
A8: 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))) ;
A9: ( 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 A8, A3, 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 A9, A5, A6, A7, A2, B1, EXTPRO_1:def 10; :: thesis: verum