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, AMI_1:def 25;
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 AMI_1:14
.= 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 AMI_1:14
.= 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, AMI_1:def 25; :: thesis: verum