open NSLPK-INIT + INV .
  -- begin of fresh constants
  op ps : -> PrinSet .
  -- end of fresh constants
  -- check that this reduces to true
  red check(true,isValid(init(ps))) .
close

open NSLPK-CHALLENGE1 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  op ps : -> PrinSet .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which CHALLENGE1 can be applied
  eq c = (nw: nw) (rand: r) (nonces: ns) (prins: (p q ps)) .
  eq (p = q) = false .
  -- check if CHALLENGE1 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config
      suchThat (not (check(isValid(c),isValid(C)))) .
close

open NSLPK-CHALLENGE2 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  op ps : -> PrinSet .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which CHALLENGE2 can be applied
  eq c = (nw: nw) (rand: r) (nonces: ns) (prins: (p ps)) .
  -- check if CHALLENGE2 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-CHALLENGE3 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  op ps : -> PrinSet .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which CHALLENGE3 can be applied
  eq c = (nw: nw) (rand: r) (nonces: ns) (prins: (q ps)) .
  -- check if CHALLENGE3 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-RESPONSE + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which RESPONSE can be applied
  eq c = (nw: (m1(pi',pi,qi,c1(qi,n,pi)) nw))
         (rand: r) (nonces: ns) (prins: ps) .
  -- check if RESPONSE can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-CONFIRMATION + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops pi qi qi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  ops n n' : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which CONFIRMATION can be applied
  eq c = (nw: (m2(qi',qi,pi,c2(pi,n,n',qi))
               m1(pi,pi,qi,c1(qi,n,pi)) nw))
         (rand: r) (nonces: ns) (prins: ps) .
  -- check if CONFIRMATION can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE11 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE11 can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n ns)) (prins: (p q ps)) .
  eq (p = q) = false .
  -- check if FAKE11 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE11a + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE11a can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n ns)) (prins: (p ps)) .
  -- check if FAKE11a can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE11b + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE11b can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n ns)) (prins: (q ps)) .
  -- check if FAKE11b can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE12 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c1 : -> Cipher1 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE12 can be applied
  eq c = (nw: (m1(pi',pi,qi,c1) nw))
         (rand: r) (nonces: ns) (prins: (p q ps)) .
  eq (p = q) = false .
  -- check if FAKE12 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE12a + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c1 : -> Cipher1 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE12a can be applied
  eq c = (nw: (m1(pi',pi,qi,c1) nw))
         (rand: r) (nonces: ns) (prins: (p ps)) .
  -- check if FAKE12a can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE12b + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c1 : -> Cipher1 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE12b can be applied
  eq c = (nw: (m1(pi',pi,qi,c1) nw))
         (rand: r) (nonces: ns) (prins: (q ps)) .
  -- check if FAKE12b can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE21 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  op ps : -> PrinSet .
  ops n n' : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE21 can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n n' ns)) (prins: (p q ps)) .
  eq (n = n') = false .
  eq (p = q) = false .
  -- check if FAKE21 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE21a + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  op ps : -> PrinSet .
  ops n n' : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE21a can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n n' ns)) (prins: (p ps)) .
  eq (n = n') = false .
  -- check if FAKE21a can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE21b + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  op ps : -> PrinSet .
  ops n n' : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE21b can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n n' ns)) (prins: (q ps)) .
  eq (n = n') = false .
  -- check if FAKE21b can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE22 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  ops pi qi qi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c2 : -> Cipher2 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE22 can be applied
  eq c = (nw: (m2(qi',qi,pi,c2) nw))
         (rand: r) (nonces: ns) (prins: (p q ps)) .
  eq (p = q) = false .
  -- check if FAKE22 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE22a + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  ops pi qi qi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c2 : -> Cipher2 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE22a can be applied
  eq c = (nw: (m2(qi',qi,pi,c2) nw))
         (rand: r) (nonces: ns) (prins: (p ps)) .
  -- check if FAKE22a can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE22b + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  ops pi qi qi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c2 : -> Cipher2 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE22b can be applied
  eq c = (nw: (m2(qi',qi,pi,c2) nw))
         (rand: r) (nonces: ns) (prins: (q ps)) .
  -- check if FAKE22b can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE31 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE31 can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n ns)) (prins: (p q ps)) .
  eq (p = q) = false .
  -- check if FAKE31 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE31a + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE31a can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n ns)) (prins: (p ps)) .
  -- check if FAKE31a can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE31b + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  op ps : -> PrinSet .
  op n : -> Nonce .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE31b can be applied
  eq c = (nw: nw) (rand: r) (nonces: (n ns)) (prins: (q ps)) .
  -- check if FAKE31b can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE32 + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  ops p q : -> Prin .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c3 : -> Cipher3 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE32 can be applied
  eq c = (nw: (m3(pi',pi,qi,c3) nw))
         (rand: r) (nonces: ns) (prins: (p q ps)) .
  eq (p = q) = false .
  -- check if FAKE32 can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE32a + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op p : -> Prin .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c3 : -> Cipher3 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE32a can be applied
  eq c = (nw: (m3(pi',pi,qi,c3) nw))
         (rand: r) (nonces: ns) (prins: (p ps)) .
  -- check if FAKE32a can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close

open NSLPK-FAKE32b + INV .
  -- begin of fresh constants
  op c : -> Config .
  op nw : -> Network .
  op r : -> PNat .
  op ns : -> NonceSet .
  op q : -> Prin .
  ops pi qi pi' : -> Prin&Intrdr .
  op ps : -> PrinSet .
  op c3 : -> Cipher3 .
  -- end of fresh constants
  -- begin of case analysis
  -- end of case analysis
  -- an arbitrary configuration to which FAKE32b can be applied
  eq c = (nw: (m3(pi',pi,qi,c3) nw))
         (rand: r) (nonces: ns) (prins: (q ps)) .
  -- check if FAKE32b can be applied to c
  red c =(*,1)=>+ C:Config .
  -- check that this reduces to false
  red c =(*,1)=>+ C:Config suchThat (not (isValid(c) implies isValid(C))) .
close