let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p holds
((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2)))
let s1, s2 be State of SCMPDS; :: thesis: ( p c= s1 & p c= s2 implies for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p holds
((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2))) )
assume A1: ( p c= s1 & p c= s2 ) ; :: thesis: for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p holds
((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2)))
let i be Element of NAT ; :: thesis: for k1, k2 being Integer
for a, b being Int_position st CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p holds
((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2)))
let k1, k2 be Integer; :: thesis: for a, b being Int_position st CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p holds
((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2)))
let a, b be Int_position ; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p implies ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2))) )
set I = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)));
set Cs1i = Comput ((ProgramPart s1),s1,i);
set Cs2i = Comput ((ProgramPart s2),s2,i);
assume that
A2: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (a,k1,b,k2) and
A3: a in dom p and
A4: DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p ; :: thesis: ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2)))
( a in dom p implies ( ((Comput ((ProgramPart s1),s1,i)) | (dom p)) . a = (Comput ((ProgramPart s1),s1,i)) . a & ((Comput ((ProgramPart s2),s2,i)) | (dom p)) . a = (Comput ((ProgramPart s2),s2,i)) . a ) ) by FUNCT_1:72;
then A5: (Comput ((ProgramPart s1),s1,i)) . a = (Comput ((ProgramPart s2),s2,i)) . a by A1, A3, EXTPRO_1:def 9;
set Cs2i1 = Comput ((ProgramPart s2),s2,(i + 1));
set Cs1i1 = Comput ((ProgramPart s1),s1,(i + 1));
set D11 = (Comput ((ProgramPart s1),s1,(i + 1))) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1));
set D21 = (Comput ((ProgramPart s2),s2,(i + 1))) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1));
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,i)) by AMI_1:123;
Comput ((ProgramPart s1),s1,(i + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i))) by T ;
then A6: (Comput ((ProgramPart s1),s1,(i + 1))) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1)) = ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) by A2, SCMPDS_2:63;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,i)) by AMI_1:123;
A7: Comput ((ProgramPart s2),s2,(i + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i)))),(Comput ((ProgramPart s2),s2,i))) by T ;
A8: ( DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1) in dom p implies ( ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom p)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1)) = (Comput ((ProgramPart s1),s1,(i + 1))) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1)) & ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom p)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1)) = (Comput ((ProgramPart s2),s2,(i + 1))) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1)) ) ) by FUNCT_1:72;
CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) by A1, Th23;
then (Comput ((ProgramPart s2),s2,(i + 1))) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1)) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2))) by A7, A2, SCMPDS_2:63;
hence ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . a),k1))) * ((Comput ((ProgramPart s1),s1,i)) . (DataLoc (((Comput ((ProgramPart s1),s1,i)) . b),k2))) = ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . a),k1))) * ((Comput ((ProgramPart s2),s2,i)) . (DataLoc (((Comput ((ProgramPart s2),s2,i)) . b),k2))) by A1, A8, A4, A5, A6, EXTPRO_1:def 9; :: thesis: verum