tamarin-prover-0.8.4.0: data/intruder_variants_dh.spthy

rule (modulo AC) cexp:
   [ !KU( x ), !KU( x.1 ) ] --[ !KU( x^x.1 ) ]-> [ !KU( x^x.1 ) ]

rule (modulo AC) cinv:
   [ !KU( x ) ] --[ !KU( inv(x) ) ]-> [ !KU( inv(x) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^x.3 ), !KU( x.1 ) ] --> [ !KD( x.2^(x.1*x.3) ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^x.2 ), !KU( inv(x.2) ) ] --> [ !KD( x.3 ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^inv(x.2) ), !KU( x.2 ) ] --> [ !KD( x.3 ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^inv(x.4) ), !KU( inv(x.2) ) ]
  -->
   [ !KD( x.3^inv((x.2*x.4)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^x.3 ), !KU( inv((x.3*x.4)) ) ] --> [ !KD( x.2^inv(x.4) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^x.3 ), !KU( (x.4*inv(x.3)) ) ] --> [ !KD( x.2^x.4 ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^inv(x.2) ), !KU( (x.2*x.3) ) ] --> [ !KD( x.4^x.3 ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^inv((x.2*x.4)) ), !KU( x.2 ) ] --> [ !KD( x.3^inv(x.4) ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^(x.2*x.4) ), !KU( inv(x.2) ) ] --> [ !KD( x.3^x.4 ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^(x.4*inv(x.2)) ), !KU( x.2 ) ] --> [ !KD( x.3^x.4 ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^inv(x.3) ), !KU( (x.4*inv(x.5)) ) ]
  -->
   [ !KD( x.2^(x.4*inv((x.3*x.5))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^(x.4*inv(x.5)) ), !KU( inv(x.2) ) ]
  -->
   [ !KD( x.3^(x.4*inv((x.2*x.5))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^x.3 ), !KU( (x.4*inv((x.3*x.5))) ) ]
  -->
   [ !KD( x.2^(x.4*inv(x.5)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^inv((x.2*x.5)) ), !KU( (x.2*x.3) ) ]
  -->
   [ !KD( x.4^(x.3*inv(x.5)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*x.5) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^(x.2*x.5) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*x.5) ), !KU( inv((x.2*x.3)) ) ]
  -->
   [ !KD( x.4^(x.5*inv(x.2)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.5*inv(x.2)) ), !KU( (x.2*x.3) ) ]
  -->
   [ !KD( x.4^(x.3*x.5) ) ]

rule (modulo AC) dexp:
   [ !KD( x.3^(x.4*inv((x.2*x.5))) ), !KU( x.2 ) ]
  -->
   [ !KD( x.3^(x.4*inv(x.5)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.5*inv(x.6)) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^(x.2*x.5*inv((x.3*x.6))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*inv(x.2)) ), !KU( (x.2*inv(x.3)) ) ] --> [ !KD( x.4 ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^inv((x.2*x.5)) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^inv((x.3*x.5)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*inv(x.5)) ), !KU( inv((x.2*x.3)) ) ]
  -->
   [ !KD( x.4^inv((x.2*x.5)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^(x.3*x.4) ), !KU( (x.5*inv((x.3*x.6))) ) ]
  -->
   [ !KD( x.2^(x.4*x.5*inv(x.6)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.5*inv((x.2*x.6))) ), !KU( (x.2*x.3) ) ]
  -->
   [ !KD( x.4^(x.3*x.5*inv(x.6)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*x.5*inv(x.2)) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^x.5 ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*inv(x.2)) ), !KU( (x.2*x.3*inv(x.4)) ) ]
  -->
   [ !KD( x.5^x.3 ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^inv((x.2*x.6)) ), !KU( (x.2*x.3*inv(x.4)) ) ]
  -->
   [ !KD( x.5^(x.3*inv((x.4*x.6))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*x.5*inv(x.6)) ), !KU( inv((x.2*x.3)) ) ]
  -->
   [ !KD( x.4^(x.5*inv((x.2*x.6))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*inv((x.2*x.5))) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^inv(x.5) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.4*inv((x.3*x.5))) ) ]
  -->
   [ !KD( x.2^inv(x.5) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*x.6*inv(x.2)) ), !KU( (x.2*x.3*inv(x.4)) ) ]
  -->
   [ !KD( x.5^(x.3*x.6) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.5*inv((x.3*x.6))) ) ]
  -->
   [ !KD( x.2^(x.5*inv((x.4*x.6))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.5*inv((x.2*x.6))) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^(x.5*inv((x.3*x.6))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*inv((x.2*x.6))) ), !KU( (x.2*x.3*inv(x.4)) ) ]
  -->
   [ !KD( x.5^(x.3*inv(x.6)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*x.6*inv(x.2)) ), !KU( (x.2*inv((x.3*x.4))) ) ]
  -->
   [ !KD( x.5^(x.6*inv(x.3)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.4*x.5*inv((x.3*x.6))) ) ]
  -->
   [ !KD( x.2^(x.5*inv(x.6)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.4^(x.3*x.5*inv((x.2*x.6))) ), !KU( (x.2*inv(x.3)) ) ]
  -->
   [ !KD( x.4^(x.5*inv(x.6)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.6*inv((x.2*x.7))) ), !KU( (x.2*x.3*inv(x.4)) ) ]
  -->
   [ !KD( x.5^(x.3*x.6*inv((x.4*x.7))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*x.6*inv(x.7)) ), !KU( (x.2*inv((x.3*x.4))) ) ]
  -->
   [ !KD( x.5^(x.2*x.6*inv((x.3*x.7))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*inv((x.2*x.6))) ), !KU( (x.2*inv((x.3*x.4))) ) ]
  -->
   [ !KD( x.5^inv((x.3*x.6)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*x.6*inv((x.2*x.7))) ), !KU( (x.2*x.3*inv(x.4)) ) ]
  -->
   [ !KD( x.5^(x.3*x.6*inv(x.7)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.2^(x.3*x.4*inv(x.5)) ), !KU( (x.5*x.6*inv((x.3*x.7))) ) ]
  -->
   [ !KD( x.2^(x.4*x.6*inv(x.7)) ) ]

rule (modulo AC) dexp:
   [ !KD( x.6^(x.5*inv((x.2*x.7))) ), !KU( (x.2*x.3*inv((x.4*x.5))) ) ]
  -->
   [ !KD( x.6^(x.3*inv((x.4*x.7))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.5^(x.4*x.6*inv((x.2*x.7))) ), !KU( (x.2*inv((x.3*x.4))) ) ]
  -->
   [ !KD( x.5^(x.6*inv((x.3*x.7))) ) ]

rule (modulo AC) dexp:
   [ !KD( x.6^(x.5*x.7*inv((x.2*x.8))) ), !KU( (x.2*x.3*inv((x.4*x.5))) ) ]
  -->
   [ !KD( x.6^(x.3*x.7*inv((x.4*x.8))) ) ]

rule (modulo AC) dinv:
   [ !KD( inv(x.1) ) ] --> [ !KD( x.1 ) ]