(herald "Plain diffie-hellman protocol with challenge-response"
  (algebra diffie-hellman))

(comment "CPSA 4.4.0")
(comment "All input read from plaindh.scm")

(defprotocol plaindh diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (n text))
    (trace (send (exp (gen) x)) (recv h) (send (enc n (exp h x)))
      (recv n))
    (uniq-orig n)
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (n text))
    (trace (recv h) (send (exp (gen) y)) (recv (enc n (exp h y)))
      (send n))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment "Diffie-hellman key exchange followed by an encryption"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx))
  (defstrand init 4 (n n) (h h) (x x))
  (uniq-orig n)
  (uniq-gen x)
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n)))
  (label 0)
  (unrealized (0 3))
  (origs (n (0 2)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h h) (x x))
  (defstrand resp 4 (n n) (h (exp h (mul x (rec y)))) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 3) (0 3)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 4) n (0 3) (enc n (exp h x)))
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n))
    ((recv (exp h (mul x (rec y)))) (send (exp (gen) y))
      (recv (enc n (exp h x))) (send n)))
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx))
  (defstrand init 4 (n n) (h h) (x x))
  (deflistener (exp h x))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)))
  (uniq-orig n)
  (uniq-gen x)
  (operation nonce-test (added-listener (exp h x)) n (0 3)
    (enc n (exp h x)))
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n))
    ((recv (exp h x)) (send (exp h x))))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton plaindh
  (vars (n text) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (uniq-orig n)
  (uniq-gen y x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 3)
  (parent 1)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (defstrand resp 4 (n n) (h (gen)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) y))))
    (gen) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))
      (send n)))
  (label 4)
  (parent 1)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x-0)) (y y))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 0) (1 0)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y x-0)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((send (exp (gen) x-0))))
  (label 5)
  (parent 1)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) y-0)) (y y))
  (defstrand resp 2 (h h) (y y-0))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y y-0)))
      (send (enc n (exp (gen) (mul y y-0)))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))) (send n))
    ((recv h) (send (exp (gen) y-0))))
  (label 6)
  (parent 1)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx) (w expt))
  (defstrand init 4 (n n) (h h) (x x))
  (defstrand resp 4 (n n) (h (exp h (mul x (rec y)))) (y y))
  (deflistener (cat (exp h (mul x (rec y) (rec w))) w))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 3) (0 3)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test
    (added-listener (cat (exp h (mul x (rec y) (rec w))) w))
    (exp h (mul x (rec y))) (1 0))
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n))
    ((recv (exp h (mul x (rec y)))) (send (exp (gen) y))
      (recv (enc n (exp h x))) (send n))
    ((recv (cat (exp h (mul x (rec y) (rec w))) w))
      (send (cat (exp h (mul x (rec y) (rec w))) w))))
  (label 7)
  (parent 1)
  (unrealized (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)))
  (uniq-orig n)
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x)))
      (recv n)) ((recv (exp (gen) x)) (send (exp (gen) x))))
  (label 8)
  (parent 2)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)))
  (uniq-orig n)
  (uniq-gen x)
  (operation nonce-test (contracted (h (exp (gen) (rec x)))) (gen)
    (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen))))
  (label 9)
  (parent 2)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)) ((2 0) (0 1)) ((2 0) (1 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) x-0)))
      (send (enc n (exp (gen) x-0))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((send (exp (gen) x-0))))
  (label 10)
  (parent 2)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)) ((2 1) (0 1)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv h) (send (exp (gen) y))))
  (label 11)
  (parent 2)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx) (w expt))
  (defstrand init 4 (n n) (h h) (x x))
  (deflistener (exp h x))
  (deflistener (cat (exp h (mul x (rec w))) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul x (rec w))) w))
    (exp h x) (1 0))
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n))
    ((recv (exp h x)) (send (exp h x)))
    ((recv (cat (exp h (mul x (rec w))) w))
      (send (cat (exp h (mul x (rec w))) w))))
  (label 12)
  (parent 2)
  (unrealized (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton plaindh
  (vars (n text) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (uniq-orig n)
  (uniq-gen x)
  (operation generalization deleted (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul y x)))) (recv n)))
  (label 13)
  (parent 3)
  (realized)
  (shape)
  (maps ((0) ((x x) (h (exp (gen) y)) (n n))))
  (origs (n (0 2))))

(defskeleton plaindh
  (vars (n text) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (defstrand resp 4 (n n) (h (gen)) (y y))
  (deflistener (cat (exp (gen) (rec x)) y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) (rec x)) y))
    (exp (gen) (mul (rec x) y)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))
      (send n))
    ((recv (cat (exp (gen) (rec x)) y))
      (send (cat (exp (gen) (rec x)) y))))
  (label 14)
  (parent 4)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (defstrand resp 4 (n n) (h (gen)) (y y))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul (rec x) y)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))
      (send n))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 15)
  (parent 4)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x-0)) (y y))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) (mul (rec x) y)) x-0))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 0) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y)) x-0))
    (exp (gen) (mul (rec x) y x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y x-0)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) (mul (rec x) y)) x-0))
      (send (cat (exp (gen) (mul (rec x) y)) x-0))))
  (label 16)
  (parent 5)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x-0)) (y y))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) (mul (rec x) x-0)) y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 0) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) x-0)) y))
    (exp (gen) (mul (rec x) y x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y x-0)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) (mul (rec x) x-0)) y))
      (send (cat (exp (gen) (mul (rec x) x-0)) y))))
  (label 17)
  (parent 5)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x-0)) (y y))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) (mul y x-0)) x))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 0) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (operation nonce-test (added-listener (cat (exp (gen) (mul y x-0)) x))
    (exp (gen) (mul (rec x) y x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y x-0)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) (mul y x-0)) x))
      (send (cat (exp (gen) (mul y x-0)) x))))
  (label 18)
  (parent 5)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) y-0)) (y y))
  (defstrand resp 2 (h h) (y y-0))
  (deflistener (cat (exp (gen) (mul (rec x) y)) y-0))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y)) y-0))
    (exp (gen) (mul (rec x) y y-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y y-0)))
      (send (enc n (exp (gen) (mul y y-0)))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))) (send n))
    ((recv h) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) (mul (rec x) y)) y-0))
      (send (cat (exp (gen) (mul (rec x) y)) y-0))))
  (label 19)
  (parent 6)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) y-0)) (y y))
  (defstrand resp 2 (h h) (y y-0))
  (deflistener (cat (exp (gen) (mul (rec x) y-0)) y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y-0)) y))
    (exp (gen) (mul (rec x) y y-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y y-0)))
      (send (enc n (exp (gen) (mul y y-0)))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))) (send n))
    ((recv h) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) (mul (rec x) y-0)) y))
      (send (cat (exp (gen) (mul (rec x) y-0)) y))))
  (label 20)
  (parent 6)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) y-0)) (y y))
  (defstrand resp 2 (h h) (y y-0))
  (deflistener (cat (exp (gen) (mul y y-0)) x))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (operation nonce-test (added-listener (cat (exp (gen) (mul y y-0)) x))
    (exp (gen) (mul (rec x) y y-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y y-0)))
      (send (enc n (exp (gen) (mul y y-0)))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))) (send n))
    ((recv h) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) (mul y y-0)) x))
      (send (cat (exp (gen) (mul y y-0)) x))))
  (label 21)
  (parent 6)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (y rndx) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y w))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul w x))) (y y))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y w)))
      (send (enc n (exp (gen) (mul y w x)))) (recv n))
    ((recv (exp (gen) (mul w x))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w x)))) (send n))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 22)
  (parent 7)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x y rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y w))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) w)) (y y))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) y w))))
    (gen) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y w)))
      (send (enc n (exp (gen) (mul y w)))) (recv n))
    ((recv (exp (gen) w)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w)))) (send n))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 23)
  (parent 7)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x y rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y w x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul w x-0))) (y y))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y w x-0)))
      (send (enc n (exp (gen) (mul y w x-0)))) (recv n))
    ((recv (exp (gen) (mul w x-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0))))
  (label 24)
  (parent 7)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx) (w expt) (y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y w y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul w y-0))) (y y))
  (deflistener (cat (exp (gen) y-0) w))
  (defstrand resp 2 (h h) (y y-0))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y w y-0)))
      (send (enc n (exp (gen) (mul y w y-0)))) (recv n))
    ((recv (exp (gen) (mul w y-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w y-0)))) (send n))
    ((recv (cat (exp (gen) y-0) w)) (send (cat (exp (gen) y-0) w)))
    ((recv h) (send (exp (gen) y-0))))
  (label 25)
  (parent 7)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (gen)) (x x))
  (uniq-orig n)
  (uniq-gen x)
  (operation generalization deleted (1 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x)))
      (recv n)))
  (label 26)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((x x) (h (gen)) (n n))))
  (origs (n (0 2))))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (exp (gen) (mul (rec x) (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) (rec w))) w))
    (exp (gen) (rec x)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (exp (gen) (mul (rec x) (rec w))) w))
      (send (cat (exp (gen) (mul (rec x) (rec w))) w))))
  (label 27)
  (parent 9)
  (unrealized (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) (rec x)) x-0))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 0) (1 0))
    ((2 0) (3 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (operation nonce-test (added-listener (cat (exp (gen) (rec x)) x-0))
    (exp (gen) (mul (rec x) x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) x-0)))
      (send (enc n (exp (gen) x-0))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) (rec x)) x-0))
      (send (cat (exp (gen) (rec x)) x-0))))
  (label 28)
  (parent 10)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 0) (1 0))
    ((2 0) (3 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (operation nonce-test (added-listener (cat (exp (gen) x-0) x))
    (exp (gen) (mul (rec x) x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) x-0)))
      (send (enc n (exp (gen) x-0))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-0) x)) (send (cat (exp (gen) x-0) x))))
  (label 29)
  (parent 10)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) (rec x)) y))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((2 1) (3 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) (rec x)) y))
    (exp (gen) (mul (rec x) y)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) (rec x)) y))
      (send (cat (exp (gen) (rec x)) y))))
  (label 30)
  (parent 11)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((2 1) (3 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul (rec x) y)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 31)
  (parent 11)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul w x)))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) w))
      (send (enc n (exp (gen) (mul w x)))) (recv n))
    ((recv (exp (gen) (mul w x))) (send (exp (gen) (mul w x))))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 32)
  (parent 12)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) w))) (x x))
  (deflistener (exp (gen) w))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) w))))
    (gen) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) w)))
      (send (enc n (exp (gen) w))) (recv n))
    ((recv (exp (gen) w)) (send (exp (gen) w)))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 33)
  (parent 12)
  (unrealized (0 1))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) w x-0))) (x x))
  (deflistener (exp (gen) (mul w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) w x-0)))
      (send (enc n (exp (gen) (mul w x-0)))) (recv n))
    ((recv (exp (gen) (mul w x-0))) (send (exp (gen) (mul w x-0))))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0))))
  (label 34)
  (parent 12)
  (unrealized (0 1))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) w y))) (x x))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) w y)))
      (send (enc n (exp (gen) (mul w y)))) (recv n))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv h) (send (exp (gen) y))))
  (label 35)
  (parent 12)
  (unrealized (0 1))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton plaindh
  (vars (n text) (y rndx) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y w))) (x x))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (1 0))
  (operation generalization deleted (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y w)))
      (send (enc n (exp (gen) (mul y w x)))) (recv n))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 36)
  (parent 22)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x)) (y y))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (displaced 3 1 resp 2) (exp (gen) y-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 37)
  (parent 23)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y rndx) (w w-0 expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y w))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) w)) (y y))
  (deflistener (cat (gen) w))
  (deflistener (cat (exp (gen) (mul (rec x) y w (rec w-0))) w-0))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y w (rec w-0))) w-0))
    (exp (gen) (mul (rec x) y w)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y w)))
      (send (enc n (exp (gen) (mul y w)))) (recv n))
    ((recv (exp (gen) w)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w)))) (send n))
    ((recv (cat (gen) w)) (send (cat (gen) w)))
    ((recv (cat (exp (gen) (mul (rec x) y w (rec w-0))) w-0))
      (send (cat (exp (gen) (mul (rec x) y w (rec w-0))) w-0))))
  (label 38)
  (parent 23)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 y rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0 y)
  (precur (2 0))
  (operation nonce-test (displaced 4 1 resp 2) (exp (gen) y-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (exp (gen) x-0))))
  (label 39)
  (parent 24)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y rndx) (w expt) (x-0 rndx) (w-0 expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y w x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul w x-0))) (y y))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) (mul (rec x) y w x-0 (rec w-0))) w-0))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (4 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 0) (2 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (added-listener
      (cat (exp (gen) (mul (rec x) y w x-0 (rec w-0))) w-0))
    (exp (gen) (mul (rec x) y w x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y w x-0)))
      (send (enc n (exp (gen) (mul y w x-0)))) (recv n))
    ((recv (exp (gen) (mul w x-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) (mul (rec x) y w x-0 (rec w-0))) w-0))
      (send (cat (exp (gen) (mul (rec x) y w x-0 (rec w-0))) w-0))))
  (label 40)
  (parent 24)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) y-0)) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x)) (y y-0))
  (deflistener (cat (exp (gen) y) (mul x (rec y))))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0))
  (operation nonce-test (displaced 4 1 resp 2) (exp (gen) y-1) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y-0))
      (send (enc n (exp (gen) (mul x y-0)))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) y-0))
      (recv (enc n (exp (gen) (mul x y-0)))) (send n))
    ((recv (cat (exp (gen) y) (mul x (rec y))))
      (send (cat (exp (gen) y) (mul x (rec y)))))
    ((recv h) (send (exp (gen) y))))
  (label 41)
  (parent 25)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx) (w expt) (y-0 rndx) (w-0 expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y w y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul w y-0))) (y y))
  (deflistener (cat (exp (gen) y-0) w))
  (defstrand resp 2 (h h) (y y-0))
  (deflistener (cat (exp (gen) (mul (rec x) y w y-0 (rec w-0))) w-0))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (4 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (added-listener
      (cat (exp (gen) (mul (rec x) y w y-0 (rec w-0))) w-0))
    (exp (gen) (mul (rec x) y w y-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y w y-0)))
      (send (enc n (exp (gen) (mul y w y-0)))) (recv n))
    ((recv (exp (gen) (mul w y-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y w y-0)))) (send n))
    ((recv (cat (exp (gen) y-0) w)) (send (cat (exp (gen) y-0) w)))
    ((recv h) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) (mul (rec x) y w y-0 (rec w-0))) w-0))
      (send (cat (exp (gen) (mul (rec x) y w y-0 (rec w-0))) w-0))))
  (label 42)
  (parent 25)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (exp (gen) x) (mul (rec x) (rec x))))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (exp (gen) x) (mul (rec x) (rec x))))
      (send (cat (exp (gen) x) (mul (rec x) (rec x))))))
  (label 43)
  (parent 27)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (rec x)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (x-0 x) (w (rec x))) (gen) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (rec x))) (send (cat (gen) (rec x)))))
  (label 44)
  (parent 27)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (exp (gen) x-0) (mul (rec x) (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (0 1))
    ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (exp (gen) x-0) (mul (rec x) (rec x-0))))
      (send (cat (exp (gen) x-0) (mul (rec x) (rec x-0)))))
    ((send (exp (gen) x-0))))
  (label 45)
  (parent 27)
  (unrealized (0 1) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (exp (gen) y) (mul (rec x) (rec y))))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (exp (gen) y) (mul (rec x) (rec y))))
      (send (cat (exp (gen) y) (mul (rec x) (rec y)))))
    ((recv h) (send (exp (gen) y))))
  (label 46)
  (parent 27)
  (unrealized (0 1) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) w)) (x x))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (1 0))
  (operation generalization deleted (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) w))
      (send (enc n (exp (gen) (mul w x)))) (recv n))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 47)
  (parent 32)
  (seen 65)
  (realized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) x)) (x x))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (gen) (mul x x)))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x))
      (send (enc n (exp (gen) (mul x x)))) (recv n))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (gen) (mul x x))) (send (cat (gen) (mul x x)))))
  (label 48)
  (parent 33)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (x-0 x) (w x)) (gen) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x)))
      (recv n)) ((recv (exp (gen) x)) (send (exp (gen) x)))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 49)
  (parent 33)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))) (recv n))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) (mul x x-0))))
    ((recv (cat (gen) (mul x x-0))) (send (cat (gen) (mul x x-0))))
    ((send (exp (gen) x-0))))
  (label 50)
  (parent 33)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y))))
    ((recv h) (send (exp (gen) y))))
  (label 51)
  (parent 33)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w w-0 expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) w))) (x x))
  (deflistener (exp (gen) w))
  (deflistener (cat (gen) w))
  (deflistener (cat (exp (gen) (mul (rec x) w (rec w-0))) w-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) w (rec w-0))) w-0))
    (exp (gen) (mul (rec x) w)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) w)))
      (send (enc n (exp (gen) w))) (recv n))
    ((recv (exp (gen) w)) (send (exp (gen) w)))
    ((recv (cat (gen) w)) (send (cat (gen) w)))
    ((recv (cat (exp (gen) (mul (rec x) w (rec w-0))) w-0))
      (send (cat (exp (gen) (mul (rec x) w (rec w-0))) w-0))))
  (label 52)
  (parent 33)
  (unrealized (3 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (displaced 4 3 init 1) (exp (gen) x-1) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))) (recv n))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) (mul x x-0))))
    ((recv (cat (exp (gen) x-0) x)) (send (cat (exp (gen) x-0) x)))
    ((send (exp (gen) x-0))))
  (label 53)
  (parent 34)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) x-0)) (x x-0))
  (deflistener (exp (gen) (mul x-0 x-0)))
  (deflistener (cat (exp (gen) x) (mul (rec x) x-0 x-0)))
  (defstrand init 1 (x x))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-1) (0 1))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x-0 x-0)))) (recv n))
    ((recv (exp (gen) (mul x-0 x-0))) (send (exp (gen) (mul x-0 x-0))))
    ((recv (cat (exp (gen) x) (mul (rec x) x-0 x-0)))
      (send (cat (exp (gen) x) (mul (rec x) x-0 x-0))))
    ((send (exp (gen) x))))
  (label 54)
  (parent 34)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test
    (contracted (x-1 x) (w (mul x (rec x-0))) (x-2 x-0)) (gen) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x)))
      (recv n)) ((recv (exp (gen) x)) (send (exp (gen) x)))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (exp (gen) x-0))))
  (label 55)
  (parent 34)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 x-1 rndx))
  (defstrand init 4 (n n) (h (exp (gen) x-1)) (x x))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
  (defstrand init 1 (x x-0))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)) ((4 0) (0 1)) ((4 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0 x-1)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-1))
      (send (enc n (exp (gen) (mul x x-1)))) (recv n))
    ((recv (exp (gen) (mul x x-1))) (send (exp (gen) (mul x x-1))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) x-1))))
    ((send (exp (gen) x-0))) ((send (exp (gen) x-1))))
  (label 56)
  (parent 34)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x x-0 y rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) y)))
  (defstrand init 1 (x x-0))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 0) (0 1))
    ((3 0) (2 0)) ((4 1) (0 1)) ((4 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0 y)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) y)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) y))))
    ((send (exp (gen) x-0))) ((recv h) (send (exp (gen) y))))
  (label 57)
  (parent 34)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (x-0 rndx) (w-0 expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) w x-0))) (x x))
  (deflistener (exp (gen) (mul w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) (mul (rec x) w x-0 (rec w-0))) w-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) w x-0 (rec w-0))) w-0))
    (exp (gen) (mul (rec x) w x-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) w x-0)))
      (send (enc n (exp (gen) (mul w x-0)))) (recv n))
    ((recv (exp (gen) (mul w x-0))) (send (exp (gen) (mul w x-0))))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) (mul (rec x) w x-0 (rec w-0))) w-0))
      (send (cat (exp (gen) (mul (rec x) w x-0 (rec w-0))) w-0))))
  (label 58)
  (parent 34)
  (unrealized (4 0))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) x-0)))
  (defstrand resp 2 (h h) (y y))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)) ((4 0) (0 1)) ((4 0) (2 0)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))) (recv n))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) (mul x x-0))))
    ((recv (cat (exp (gen) y) (mul x (rec y) x-0)))
      (send (cat (exp (gen) y) (mul x (rec y) x-0))))
    ((recv h) (send (exp (gen) y))) ((send (exp (gen) x-0))))
  (label 59)
  (parent 35)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) x)) (x x))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (exp (gen) y) (mul (rec y) x x)))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0))
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x))
      (send (enc n (exp (gen) (mul x x)))) (recv n))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (exp (gen) y) (mul (rec y) x x)))
      (send (cat (exp (gen) y) (mul (rec y) x x))))
    ((recv h) (send (exp (gen) y))))
  (label 60)
  (parent 35)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (deflistener (cat (exp (gen) y) (mul x (rec y))))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (contracted (x-0 x) (w (mul x (rec y))) (y-0 y))
    (gen) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x)))
      (recv n)) ((recv (exp (gen) x)) (send (exp (gen) x)))
    ((recv (cat (exp (gen) y) (mul x (rec y))))
      (send (cat (exp (gen) y) (mul x (rec y)))))
    ((recv h) (send (exp (gen) y))))
  (label 61)
  (parent 35)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (displaced 4 3 resp 2) (exp (gen) y-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((recv h) (send (exp (gen) y))))
  (label 62)
  (parent 35)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h h-0 base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) y-0)) (x x))
  (deflistener (exp (gen) (mul x y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) y-0)))
  (defstrand resp 2 (h h) (y y))
  (defstrand resp 2 (h h-0) (y y-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)) ((4 1) (0 1)) ((4 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y-0))
      (send (enc n (exp (gen) (mul x y-0)))) (recv n))
    ((recv (exp (gen) (mul x y-0))) (send (exp (gen) (mul x y-0))))
    ((recv (cat (exp (gen) y) (mul x (rec y) y-0)))
      (send (cat (exp (gen) y) (mul x (rec y) y-0))))
    ((recv h) (send (exp (gen) y))) ((recv h-0) (send (exp (gen) y-0))))
  (label 63)
  (parent 35)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx) (w expt) (y rndx) (w-0 expt))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) w y))) (x x))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) (mul (rec x) w y (rec w-0))) w-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) w y (rec w-0))) w-0))
    (exp (gen) (mul (rec x) w y)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) w y)))
      (send (enc n (exp (gen) (mul w y)))) (recv n))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) (mul (rec x) w y (rec w-0))) w-0))
      (send (cat (exp (gen) (mul (rec x) w y (rec w-0))) w-0))))
  (label 64)
  (parent 35)
  (unrealized (4 0))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton plaindh
  (vars (n text) (y rndx) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y w))) (x x))
  (uniq-orig n)
  (uniq-gen x)
  (operation generalization deleted (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y w)))
      (send (enc n (exp (gen) (mul y w x)))) (recv n)))
  (label 65)
  (parent 36)
  (realized)
  (shape)
  (maps ((0) ((x x) (h (exp (gen) (mul y w))) (n n))))
  (origs (n (0 2))))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul x w))) (y y))
  (deflistener (cat (gen) (mul x w)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (3 0))
  (operation nonce-test (displaced 4 1 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul x w y)))) (send n))
    ((recv (cat (gen) (mul x w))) (send (cat (gen) (mul x w))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 66)
  (parent 38)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul x w))) (y y))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) w)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (4 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 0) (2 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0 y)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 1 resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul x w y)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) w)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) w))))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 67)
  (parent 40)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx) (w expt) (y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul x w))) (y y-0))
  (deflistener (cat (exp (gen) y) (mul x (rec y) w)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y-0) w))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (4 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 1 resp 2) (exp (gen) y-1) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y-0)))
      (send (enc n (exp (gen) (mul x w y-0)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) y-0))
      (recv (enc n (exp (gen) (mul x w y-0)))) (send n))
    ((recv (cat (exp (gen) y) (mul x (rec y) w)))
      (send (cat (exp (gen) y) (mul x (rec y) w))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y-0) w)) (send (cat (exp (gen) y-0) w))))
  (label 68)
  (parent 42)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (exp (gen) x) (mul (rec x) (rec x))))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener x) (mul (rec x) (rec x)) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (exp (gen) x) (mul (rec x) (rec x))))
      (send (cat (exp (gen) x) (mul (rec x) (rec x)))))
    ((recv x) (send x)))
  (label 69)
  (parent 43)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (rec x)))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener x) (rec x) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (rec x))) (send (cat (gen) (rec x))))
    ((recv x) (send x)))
  (label 70)
  (parent 44)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) x)) (x x))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (gen) (mul x x)))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0)) ((3 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener x) (mul x x) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x))
      (send (enc n (exp (gen) (mul x x)))) (recv n))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (gen) (mul x x))) (send (cat (gen) (mul x x))))
    ((recv x) (send x)))
  (label 71)
  (parent 48)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x))) (x x))
  (deflistener (exp (gen) (mul w x x)))
  (deflistener (cat (gen) (mul w x x)))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-0) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x)))
      (send (enc n (exp (gen) (mul w x x)))) (recv n))
    ((recv (exp (gen) (mul w x x))) (send (exp (gen) (mul w x x))))
    ((recv (cat (gen) (mul w x x))) (send (cat (gen) (mul w x x))))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 72)
  (parent 52)
  (unrealized (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul x w)))
  (deflistener (cat (gen) (mul x w)))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (contracted (x-0 x) (w-0 (mul x w)) (w-1 w))
    (gen) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) w))
      (send (enc n (exp (gen) (mul x w)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) (mul x w))))
    ((recv (cat (gen) (mul x w))) (send (cat (gen) (mul x w))))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 73)
  (parent 52)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x-0))) (x x))
  (deflistener (exp (gen) (mul x w x-0)))
  (deflistener (cat (gen) (mul x w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 0) (2 0)) ((4 0) (3 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (3 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x-0)))
      (send (enc n (exp (gen) (mul x w x-0)))) (recv n))
    ((recv (exp (gen) (mul x w x-0))) (send (exp (gen) (mul x w x-0))))
    ((recv (cat (gen) (mul x w x-0))) (send (cat (gen) (mul x w x-0))))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0))))
  (label 74)
  (parent 52)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (gen) y))
  (deflistener (cat (exp (gen) y) (rec x)))
  (precedes ((0 0) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (3 0))
  (operation nonce-test (displaced 4 1 resp 2) (exp (gen) y) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (gen) y)) (send (cat (gen) y)))
    ((recv (cat (exp (gen) y) (rec x)))
      (send (cat (exp (gen) y) (rec x)))))
  (label 75)
  (parent 52)
  (unrealized (0 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (deflistener (exp (gen) (mul x w y)))
  (deflistener (cat (gen) (mul x w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (2 0)) ((4 1) (3 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (3 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w y))) (send (exp (gen) (mul x w y))))
    ((recv (cat (gen) (mul x w y))) (send (cat (gen) (mul x w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv h) (send (exp (gen) y))))
  (label 76)
  (parent 52)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x-0))) (x x))
  (deflistener (exp (gen) (mul x w x-0)))
  (deflistener (cat (exp (gen) x-0) (mul x w)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) x-0) w))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 3 init 1) (exp (gen) x-1) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x-0)))
      (send (enc n (exp (gen) (mul x w x-0)))) (recv n))
    ((recv (exp (gen) (mul x w x-0))) (send (exp (gen) (mul x w x-0))))
    ((recv (cat (exp (gen) x-0) (mul x w)))
      (send (cat (exp (gen) x-0) (mul x w)))) ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w))))
  (label 77)
  (parent 58)
  (unrealized (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x-0))) (x x-0))
  (deflistener (exp (gen) (mul w x-0 x-0)))
  (deflistener (cat (exp (gen) x) (mul (rec x) w x-0 x-0)))
  (defstrand init 1 (x x))
  (deflistener (cat (exp (gen) x-0) w))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 0 init 1) (exp (gen) x-1) (4 0))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) (mul w x-0)))
      (send (enc n (exp (gen) (mul w x-0 x-0)))) (recv n))
    ((recv (exp (gen) (mul w x-0 x-0)))
      (send (exp (gen) (mul w x-0 x-0))))
    ((recv (cat (exp (gen) x) (mul (rec x) w x-0 x-0)))
      (send (cat (exp (gen) x) (mul (rec x) w x-0 x-0))))
    ((send (exp (gen) x)))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w))))
  (label 78)
  (parent 58)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul x w)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) w)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-1 x) (w-0 (mul x (rec x-0) w)) (x-2 x-0) (w-1 w))
    (gen) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) w))
      (send (enc n (exp (gen) (mul x w)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) (mul x w))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) w)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) w))))
    ((send (exp (gen) x-0)))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 79)
  (parent 58)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx) (w expt) (x-1 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x-1))) (x x))
  (deflistener (exp (gen) (mul x w x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) w x-1)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) x-1) w))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((5 0) (2 0))
    ((5 0) (4 0)))
  (uniq-orig n)
  (uniq-gen x x-0 x-1)
  (precur (2 0) (4 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x-1)))
      (send (enc n (exp (gen) (mul x w x-1)))) (recv n))
    ((recv (exp (gen) (mul x w x-1))) (send (exp (gen) (mul x w x-1))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) w x-1)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) w x-1))))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-1) w)) (send (cat (exp (gen) x-1) w)))
    ((send (exp (gen) x-1))))
  (label 80)
  (parent 58)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x-0)))) (x x-0))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) x) (mul (rec x) y)))
  (defstrand init 1 (x x))
  (deflistener (cat (exp (gen) y) (rec x-0)))
  (precedes ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (1 0)) ((3 0) (2 0))
    ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 1 resp 2) (exp (gen) y) (4 0))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) (mul y (rec x-0))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) x) (mul (rec x) y)))
      (send (cat (exp (gen) x) (mul (rec x) y)))) ((send (exp (gen) x)))
    ((recv (cat (exp (gen) y) (rec x-0)))
      (send (cat (exp (gen) y) (rec x-0)))))
  (label 81)
  (parent 58)
  (unrealized (0 1) (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x x-0 rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (deflistener (exp (gen) (mul x w y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) w y)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((5 1) (2 0))
    ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen x x-0 y)
  (precur (2 0) (4 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w y))) (send (exp (gen) (mul x w y))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) w y)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) w y))))
    ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv h) (send (exp (gen) y))))
  (label 82)
  (parent 58)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x-0))) (x x))
  (deflistener (exp (gen) (mul x w x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) w x-0)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)) ((5 0) (2 0))
    ((5 0) (4 0)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x-0)))
      (send (enc n (exp (gen) (mul x w x-0)))) (recv n))
    ((recv (exp (gen) (mul x w x-0))) (send (exp (gen) (mul x w x-0))))
    ((recv (cat (exp (gen) y) (mul x (rec y) w x-0)))
      (send (cat (exp (gen) y) (mul x (rec y) w x-0))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0))))
  (label 83)
  (parent 64)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (y rndx) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x))) (x x))
  (deflistener (exp (gen) (mul w x x)))
  (deflistener (cat (exp (gen) y) (mul (rec y) w x x)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 0 init 1) (exp (gen) x-0) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x)))
      (send (enc n (exp (gen) (mul w x x)))) (recv n))
    ((recv (exp (gen) (mul w x x))) (send (exp (gen) (mul w x x))))
    ((recv (cat (exp (gen) y) (mul (rec y) w x x)))
      (send (cat (exp (gen) y) (mul (rec y) w x x))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 84)
  (parent 64)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul x w)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) w)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-0 x) (w-0 (mul x (rec y) w)) (y-0 y) (w-1 w)) (gen)
    (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) w))
      (send (enc n (exp (gen) (mul x w)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) (mul x w))))
    ((recv (cat (exp (gen) y) (mul x (rec y) w)))
      (send (cat (exp (gen) y) (mul x (rec y) w))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 85)
  (parent 64)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (y y-0 x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y-0 (rec x)))) (x x))
  (deflistener (exp (gen) y-0))
  (deflistener (cat (exp (gen) y) (mul (rec y) y-0)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y-0) (rec x)))
  (precedes ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y y-0 x)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 1 resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y-0 (rec x))))
      (send (enc n (exp (gen) y-0))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) y) (mul (rec y) y-0)))
      (send (cat (exp (gen) y) (mul (rec y) y-0))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y-0) (rec x)))
      (send (cat (exp (gen) y-0) (rec x)))))
  (label 86)
  (parent 64)
  (unrealized (0 1) (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (deflistener (exp (gen) (mul x w y)))
  (deflistener (cat (exp (gen) y) (mul x w)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (4 0))
  (operation nonce-test (displaced 5 3 resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w y))) (send (exp (gen) (mul x w y))))
    ((recv (cat (exp (gen) y) (mul x w)))
      (send (cat (exp (gen) y) (mul x w))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 87)
  (parent 64)
  (unrealized (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h h-0 base) (x y rndx) (w expt) (y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y-0))) (x x))
  (deflistener (exp (gen) (mul x w y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) w y-0)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y-0) w))
  (defstrand resp 2 (h h-0) (y y-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)) ((5 1) (2 0))
    ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0) (4 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y-0)))
      (send (enc n (exp (gen) (mul x w y-0)))) (recv n))
    ((recv (exp (gen) (mul x w y-0))) (send (exp (gen) (mul x w y-0))))
    ((recv (cat (exp (gen) y) (mul x (rec y) w y-0)))
      (send (cat (exp (gen) y) (mul x (rec y) w y-0))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y-0) w)) (send (cat (exp (gen) y-0) w)))
    ((recv h-0) (send (exp (gen) y-0))))
  (label 88)
  (parent 64)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (defstrand resp 4 (n n) (h (gen)) (y y))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (exp (gen) y) (rec x)))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (3 0))
  (operation nonce-test (contracted (x-0 x) (w (rec x))) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))
      (send n)) ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (exp (gen) y) (rec x)))
      (send (cat (exp (gen) y) (rec x)))))
  (label 89)
  (parent 66)
  (unrealized (0 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul x w))) (y y))
  (deflistener (cat (gen) (mul x w)))
  (deflistener (cat (exp (gen) y) w))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 2) (1 2)) ((1 1) (3 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (0 1)) ((4 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (mul x w) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul x w y)))) (send n))
    ((recv (cat (gen) (mul x w))) (send (cat (gen) (mul x w))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv x) (send x)))
  (label 90)
  (parent 66)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (y x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x) x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) x-0)) (y y))
  (deflistener (cat (exp (gen) x-0) (one)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (4 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 0) (2 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-1 x) (x-2 x-0) (w (mul (rec x) x-0))) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x) x-0)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) (one)))
      (send (cat (exp (gen) x-0) (one)))) ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 91)
  (parent 67)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (y x y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x) y-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (cat (exp (gen) y-0) (one)))
  (defstrand resp 2 (h h) (y y-0))
  (deflistener (cat (exp (gen) y) (mul (rec x) y-0)))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((1 1) (4 0)) ((1 3) (0 3))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x y-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-0 x) (y-1 y-0) (w (mul (rec x) y-0))) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x) y-0)))
      (send (enc n (exp (gen) (mul y y-0)))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))) (send n))
    ((recv (cat (exp (gen) y-0) (one)))
      (send (cat (exp (gen) y-0) (one))))
    ((recv h) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) y) (mul (rec x) y-0)))
      (send (cat (exp (gen) y) (mul (rec x) y-0)))))
  (label 92)
  (parent 68)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (exp (gen) x) (mul (rec x) (rec x))))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (contracted (w (mul (rec x) (rec x))) (x-0 x))
    (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (exp (gen) x) (mul (rec x) (rec x))))
      (send (cat (exp (gen) x) (mul (rec x) (rec x))))))
  (label 93)
  (parent 72)
  (unrealized (0 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (w expt) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x))) (x x))
  (deflistener (exp (gen) (mul w x x)))
  (deflistener (cat (gen) (mul w x x)))
  (deflistener (cat (exp (gen) x) w))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (mul w x x) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x)))
      (send (enc n (exp (gen) (mul w x x)))) (recv n))
    ((recv (exp (gen) (mul w x x))) (send (exp (gen) (mul w x x))))
    ((recv (cat (gen) (mul w x x))) (send (cat (gen) (mul w x x))))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w)))
    ((recv x) (send x)))
  (label 94)
  (parent 72)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (gen) (rec x)))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (contracted (x-0 x) (w (rec x))) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (gen) (rec x))) (send (cat (gen) (rec x)))))
  (label 95)
  (parent 73)
  (unrealized (0 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt))
  (defstrand init 4 (n n) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul x w)))
  (deflistener (cat (gen) (mul x w)))
  (deflistener (cat (gen) w))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (mul x w) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) w))
      (send (enc n (exp (gen) (mul x w)))) (recv n))
    ((recv (exp (gen) (mul x w))) (send (exp (gen) (mul x w))))
    ((recv (cat (gen) (mul x w))) (send (cat (gen) (mul x w))))
    ((recv (cat (gen) w)) (send (cat (gen) w))) ((recv x) (send x)))
  (label 96)
  (parent 73)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (exp (gen) x-0) (mul (rec x) (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 0) (2 0)) ((4 0) (3 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (3 0))
  (operation nonce-test
    (contracted (x-1 x) (w (mul (rec x) (rec x-0))) (x-2 x-0)) (one)
    (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (exp (gen) x-0) (mul (rec x) (rec x-0))))
      (send (cat (exp (gen) x-0) (mul (rec x) (rec x-0)))))
    ((send (exp (gen) x-0))))
  (label 97)
  (parent 74)
  (unrealized (0 1) (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (gen) y))
  (deflistener (cat (exp (gen) y) (rec x)))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (3 0)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (rec x) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (gen) y)) (send (cat (gen) y)))
    ((recv (cat (exp (gen) y) (rec x)))
      (send (cat (exp (gen) y) (rec x)))) ((recv x) (send x)))
  (label 98)
  (parent 75)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (exp (gen) y) (mul (rec x) (rec y))))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (2 0)) ((4 1) (3 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (3 0))
  (operation nonce-test
    (contracted (x-0 x) (w (mul (rec x) (rec y))) (y-0 y)) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (exp (gen) y) (mul (rec x) (rec y))))
      (send (cat (exp (gen) y) (mul (rec x) (rec y)))))
    ((recv h) (send (exp (gen) y))))
  (label 99)
  (parent 76)
  (unrealized (0 1) (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul x (rec x-0)))) (x x-0))
  (deflistener (exp (gen) x))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand init 1 (x x))
  (deflistener (cat (exp (gen) x) (rec x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (contracted (x-1 x-0) (w (rec x-0))) (one)
    (2 0))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) (mul x (rec x-0))))
      (send (enc n (exp (gen) x))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) x)))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((send (exp (gen) x)))
    ((recv (cat (exp (gen) x) (rec x-0)))
      (send (cat (exp (gen) x) (rec x-0)))))
  (label 100)
  (parent 77)
  (unrealized (0 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w x-0))) (x x))
  (deflistener (exp (gen) (mul x w x-0)))
  (deflistener (cat (exp (gen) x-0) (mul x w)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) x-0) w))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((5 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (added-listener x) (mul x w) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w x-0)))
      (send (enc n (exp (gen) (mul x w x-0)))) (recv n))
    ((recv (exp (gen) (mul x w x-0))) (send (exp (gen) (mul x w x-0))))
    ((recv (cat (exp (gen) x-0) (mul x w)))
      (send (cat (exp (gen) x-0) (mul x w)))) ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((recv x) (send x)))
  (label 101)
  (parent 77)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul x (rec x-0)))) (x x-0))
  (deflistener (exp (gen) x))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand init 1 (x x))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) (rec x-0))))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-1 x) (w (mul x (rec x-0) (rec x-0))) (x-2 x-0)) (one)
    (2 0))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) (mul x (rec x-0))))
      (send (enc n (exp (gen) x))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) x)))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((send (exp (gen) x)))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) (rec x-0))))))
  (label 102)
  (parent 78)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (deflistener (cat (exp (gen) x-0) (one)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (gen) (mul (rec x) x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-1 x) (x-2 x-0) (w (mul (rec x) x-0))) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) x-0)))
      (send (enc n (exp (gen) x-0))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-0) (one)))
      (send (cat (exp (gen) x-0) (one)))) ((send (exp (gen) x-0)))
    ((recv (cat (gen) (mul (rec x) x-0)))
      (send (cat (gen) (mul (rec x) x-0)))))
  (label 103)
  (parent 79)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 x-1 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (deflistener (cat (exp (gen) x-0) (one)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) x-1) (mul (rec x) x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((5 0) (2 0))
    ((5 0) (4 0)))
  (uniq-orig n)
  (uniq-gen x x-0 x-1)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-2 x) (x-3 x-0) (w (mul (rec x) x-0 (rec x-1)))
      (x-4 x-1)) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) x-0)))
      (send (enc n (exp (gen) x-0))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-0) (one)))
      (send (cat (exp (gen) x-0) (one)))) ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-1) (mul (rec x) x-0 (rec x-1))))
      (send (cat (exp (gen) x-1) (mul (rec x) x-0 (rec x-1)))))
    ((send (exp (gen) x-1))))
  (label 104)
  (parent 80)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x-0)))) (x x-0))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) x) (mul (rec x) y)))
  (defstrand init 1 (x x))
  (deflistener (cat (exp (gen) y) (rec x-0)))
  (deflistener x-0)
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (4 0)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 1) (0 1)) ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (added-listener x-0) (rec x-0) (4 0))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) (mul y (rec x-0))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) x) (mul (rec x) y)))
      (send (cat (exp (gen) x) (mul (rec x) y)))) ((send (exp (gen) x)))
    ((recv (cat (exp (gen) y) (rec x-0)))
      (send (cat (exp (gen) y) (rec x-0)))) ((recv x-0) (send x-0)))
  (label 105)
  (parent 81)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x x-0 y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (deflistener (cat (exp (gen) x-0) (one)))
  (defstrand init 1 (x x-0))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0 (rec y))))
  (defstrand resp 2 (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((5 1) (2 0))
    ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen x x-0 y)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-1 x) (x-2 x-0) (w (mul (rec x) x-0 (rec y))) (y-0 y))
    (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) x-0)))
      (send (enc n (exp (gen) x-0))) (recv n))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((recv (cat (exp (gen) x-0) (one)))
      (send (cat (exp (gen) x-0) (one)))) ((send (exp (gen) x-0)))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0 (rec y))))
      (send (cat (exp (gen) y) (mul (rec x) x-0 (rec y)))))
    ((recv h) (send (exp (gen) y))))
  (label 106)
  (parent 82)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) x-0) (mul (rec x) y (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)) ((5 0) (2 0))
    ((5 0) (4 0)))
  (uniq-orig n)
  (uniq-gen x y x-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-1 x) (y-0 y) (w (mul (rec x) y (rec x-0))) (x-2 x-0))
    (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) x-0) (mul (rec x) y (rec x-0))))
      (send (cat (exp (gen) x-0) (mul (rec x) y (rec x-0)))))
    ((send (exp (gen) x-0))))
  (label 107)
  (parent 83)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) x) (mul y (rec x) (rec x))))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (y-0 y) (w (mul y (rec x) (rec x))) (x-0 x)) (one)
    (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) x) (mul y (rec x) (rec x))))
      (send (cat (exp (gen) x) (mul y (rec x) (rec x))))))
  (label 108)
  (parent 84)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (x y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (gen) (mul (rec x) y)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (4 0))
  (operation nonce-test (contracted (x-0 x) (y-0 y) (w (mul (rec x) y)))
    (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (gen) (mul (rec x) y)))
      (send (cat (gen) (mul (rec x) y)))))
  (label 109)
  (parent 85)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (y y-0 x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y-0 (rec x)))) (x x))
  (deflistener (exp (gen) y-0))
  (deflistener (cat (exp (gen) y) (mul (rec y) y-0)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y-0) (rec x)))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (4 0)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (0 1)) ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen y y-0 x)
  (precur (2 0) (4 0))
  (operation nonce-test (added-listener x) (rec x) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y-0 (rec x))))
      (send (enc n (exp (gen) y-0))) (recv n))
    ((recv (exp (gen) y-0)) (send (exp (gen) y-0)))
    ((recv (cat (exp (gen) y) (mul (rec y) y-0)))
      (send (cat (exp (gen) y) (mul (rec y) y-0))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y-0) (rec x)))
      (send (cat (exp (gen) y-0) (rec x)))) ((recv x) (send x)))
  (label 110)
  (parent 86)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y) (rec x)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (4 0))
  (operation nonce-test (contracted (x-0 x) (w (rec x))) (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (rec x)))
      (send (cat (exp (gen) y) (rec x)))))
  (label 111)
  (parent 87)
  (unrealized (0 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton plaindh
  (vars (n text) (h base) (x rndx) (w expt) (y rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul w y))) (x x))
  (deflistener (exp (gen) (mul x w y)))
  (deflistener (cat (exp (gen) y) (mul x w)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y) w))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)) ((5 1) (2 0)))
  (uniq-orig n)
  (uniq-gen x y)
  (precur (2 0) (4 0))
  (operation nonce-test (added-listener x) (mul x w) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul w y)))
      (send (enc n (exp (gen) (mul x w y)))) (recv n))
    ((recv (exp (gen) (mul x w y))) (send (exp (gen) (mul x w y))))
    ((recv (cat (exp (gen) y) (mul x w)))
      (send (cat (exp (gen) y) (mul x w))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv x) (send x)))
  (label 112)
  (parent 87)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h h-0 base) (x y y-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y-0) (mul (rec x) y (rec y-0))))
  (defstrand resp 2 (h h-0) (y y-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)) ((5 1) (2 0))
    ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen x y y-0)
  (precur (2 0) (4 0))
  (operation nonce-test
    (contracted (x-0 x) (y-1 y) (w (mul (rec x) y (rec y-0))) (y-2 y-0))
    (one) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y)))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y-0) (mul (rec x) y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul (rec x) y (rec y-0)))))
    ((recv h-0) (send (exp (gen) y-0))))
  (label 113)
  (parent 88)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (defstrand resp 4 (n n) (h (gen)) (y y))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (exp (gen) y) (rec x)))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((0 2) (1 2)) ((1 1) (3 0))
    ((1 3) (0 3)) ((2 1) (1 0)) ((3 1) (0 1)) ((4 1) (3 0)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (rec x) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))
      (send n)) ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (exp (gen) y) (rec x)))
      (send (cat (exp (gen) y) (rec x)))) ((recv x) (send x)))
  (label 114)
  (parent 89)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (exp (gen) x) (mul (rec x) (rec x))))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (mul (rec x) (rec x)) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (exp (gen) x) (mul (rec x) (rec x))))
      (send (cat (exp (gen) x) (mul (rec x) (rec x)))))
    ((recv x) (send x)))
  (label 115)
  (parent 93)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (deflistener (cat (gen) (one)))
  (deflistener (cat (gen) (rec x)))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (uniq-orig n)
  (uniq-gen x)
  (precur (2 0) (3 0))
  (operation nonce-test (added-listener x) (rec x) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (rec x)))
      (send (enc n (gen))) (recv n)) ((recv (gen)) (send (gen)))
    ((recv (cat (gen) (one))) (send (cat (gen) (one))))
    ((recv (cat (gen) (rec x))) (send (cat (gen) (rec x))))
    ((recv x) (send x)))
  (label 116)
  (parent 95)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (x x-0 rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul x (rec x-0)))) (x x-0))
  (deflistener (exp (gen) x))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand init 1 (x x))
  (deflistener (cat (exp (gen) x) (rec x-0)))
  (deflistener x-0)
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen x x-0)
  (precur (2 0) (4 0))
  (operation nonce-test (added-listener x-0) (rec x-0) (4 0))
  (traces
    ((send (exp (gen) x-0)) (recv (exp (gen) (mul x (rec x-0))))
      (send (enc n (exp (gen) x))) (recv n))
    ((recv (exp (gen) x)) (send (exp (gen) x)))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((send (exp (gen) x)))
    ((recv (cat (exp (gen) x) (rec x-0)))
      (send (cat (exp (gen) x) (rec x-0)))) ((recv x-0) (send x-0)))
  (label 117)
  (parent 100)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton plaindh
  (vars (n text) (h base) (y x rndx))
  (defstrand init 4 (n n) (h (exp (gen) (mul y (rec x)))) (x x))
  (deflistener (exp (gen) y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand resp 2 (h h) (y y))
  (deflistener (cat (exp (gen) y) (rec x)))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 3)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((4 1) (0 1)) ((5 1) (4 0)))
  (uniq-orig n)
  (uniq-gen y x)
  (precur (2 0) (4 0))
  (operation nonce-test (added-listener x) (rec x) (4 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x))))
      (send (enc n (exp (gen) y))) (recv n))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((recv h) (send (exp (gen) y)))
    ((recv (cat (exp (gen) y) (rec x)))
      (send (cat (exp (gen) y) (rec x)))) ((recv x) (send x)))
  (label 118)
  (parent 111)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")