(line (spec (line (declare (line (type (line "S" 2 8 2 9 "otwayrees2.eva") (line "principal" 2 12 2 21 "otwayrees2.eva")) 2 2 2 21 "otwayrees2.eva") (line (type (line "B" 2 5 2 6 "otwayrees2.eva") (line "principal" 2 12 2 21 "otwayrees2.eva")) 2 2 2 21 "otwayrees2.eva") (line (type (line "A" 2 2 2 3 "otwayrees2.eva") (line "principal" 2 12 2 21 "otwayrees2.eva")) 2 2 2 21 "otwayrees2.eva") (line (type (line "Kab" 3 12 3 15 "otwayrees2.eva") (line "number" 3 18 3 24 "otwayrees2.eva")) 3 2 3 24 "otwayrees2.eva") (line (type (line "Kbs" 3 7 3 10 "otwayrees2.eva") (line "number" 3 18 3 24 "otwayrees2.eva")) 3 2 3 24 "otwayrees2.eva") (line (type (line "Kas" 3 2 3 5 "otwayrees2.eva") (line "number" 3 18 3 24 "otwayrees2.eva")) 3 2 3 24 "otwayrees2.eva") (line (basetype (line "key" 5 11 5 14 "otwayrees2.eva")) 5 2 5 14 "otwayrees2.eva") (line (type (line "Nb" 7 9 7 11 "otwayrees2.eva") (line "key" 7 14 7 17 "otwayrees2.eva")) 7 2 7 17 "otwayrees2.eva") (line (type (line "Na" 7 5 7 7 "otwayrees2.eva") (line "key" 7 14 7 17 "otwayrees2.eva")) 7 2 7 17 "otwayrees2.eva") (line (type (line "N" 7 2 7 3 "otwayrees2.eva") (line "key" 7 14 7 17 "otwayrees2.eva")) 7 2 7 17 "otwayrees2.eva") (line (type (line "shr" 9 2 9 5 "otwayrees2.eva") (line (secret-function (line "number" 9 20 9 26 "otwayrees2.eva") (line "principal" 9 7 9 16 "otwayrees2.eva")) 9 6 9 33 "otwayrees2.eva")) 9 2 9 33 "otwayrees2.eva") (line (everybody-knows (line "shr" 10 18 10 21 "otwayrees2.eva")) 10 2 10 21 "otwayrees2.eva") (line (alias (line "Kas" 11 8 11 11 "otwayrees2.eva") (line (apply (line "shr" 11 14 11 17 "otwayrees2.eva") (line "A" 11 18 11 19 "otwayrees2.eva")) 11 14 11 20 "otwayrees2.eva")) 11 2 11 20 "otwayrees2.eva") (line (alias (line "Kbs" 12 8 12 11 "otwayrees2.eva") (line (apply (line "shr" 12 14 12 17 "otwayrees2.eva") (line "B" 12 18 12 19 "otwayrees2.eva")) 12 14 12 20 "otwayrees2.eva")) 12 2 12 20 "otwayrees2.eva") (line (knows (line "A" 14 2 14 3 "otwayrees2.eva") (line "A" 14 10 14 11 "otwayrees2.eva")) 14 2 14 14 "otwayrees2.eva") (line (knows (line "A" 14 2 14 3 "otwayrees2.eva") (line "B" 14 13 14 14 "otwayrees2.eva")) 14 2 14 14 "otwayrees2.eva") (line (knows (line "B" 15 2 15 3 "otwayrees2.eva") (line "S" 15 10 15 11 "otwayrees2.eva")) 15 2 15 11 "otwayrees2.eva") (line (type (line "s" 17 8 17 9 "otwayrees2.eva") (line "principal" 17 12 17 21 "otwayrees2.eva")) 17 2 17 21 "otwayrees2.eva") (line (type (line "b" 17 5 17 6 "otwayrees2.eva") (line "principal" 17 12 17 21 "otwayrees2.eva")) 17 2 17 21 "otwayrees2.eva") (line (type (line "a" 17 2 17 3 "otwayrees2.eva") (line "principal" 17 12 17 21 "otwayrees2.eva")) 17 2 17 21 "otwayrees2.eva")) 1 0 17 21 "") (line (line (block (line (comm "1." (line "A" 20 7 20 8 "otwayrees2.eva") (line "B" 20 12 20 13 "otwayrees2.eva") (line (tuple (line "N" 20 16 20 17 "otwayrees2.eva") (line "A" 20 19 20 20 "otwayrees2.eva") (line "B" 20 22 20 23 "otwayrees2.eva") (line (crypt (line (tuple (line "Na" 20 26 20 28 "otwayrees2.eva") (line "N" 20 30 20 31 "otwayrees2.eva") (line "A" 20 33 20 34 "otwayrees2.eva") (line "B" 20 36 20 37 "otwayrees2.eva")) 20 26 20 37 "otwayrees2.eva") (line "Kas" 20 39 20 42 "otwayrees2.eva") (vanilla)) 20 25 20 42 "otwayrees2.eva")) 20 16 20 42 "otwayrees2.eva")) 20 4 20 42 "otwayrees2.eva") (line (comm "2." (line "B" 21 7 21 8 "otwayrees2.eva") (line "S" 21 12 21 13 "otwayrees2.eva") (line (tuple (line "N" 21 16 21 17 "otwayrees2.eva") (line "A" 21 19 21 20 "otwayrees2.eva") (line "B" 21 22 21 23 "otwayrees2.eva") (line (crypt (line (tuple (line "Na" 21 26 21 28 "otwayrees2.eva") (line "N" 21 30 21 31 "otwayrees2.eva") (line "A" 21 33 21 34 "otwayrees2.eva") (line "B" 21 36 21 37 "otwayrees2.eva")) 21 26 21 37 "otwayrees2.eva") (line "Kas" 21 39 21 42 "otwayrees2.eva") (vanilla)) 21 25 21 42 "otwayrees2.eva") (line (crypt (line (tuple (line "Nb" 22 26 22 28 "otwayrees2.eva") (line "N" 22 30 22 31 "otwayrees2.eva") (line "A" 22 33 22 34 "otwayrees2.eva") (line "B" 22 36 22 37 "otwayrees2.eva")) 22 26 22 37 "otwayrees2.eva") (line "Kbs" 22 39 22 42 "otwayrees2.eva") (vanilla)) 22 25 22 42 "otwayrees2.eva")) 21 16 22 42 "otwayrees2.eva")) 21 4 22 42 "otwayrees2.eva") (line (comm "3." (line "S" 23 7 23 8 "otwayrees2.eva") (line "B" 23 12 23 13 "otwayrees2.eva") (line (tuple (line "N" 23 16 23 17 "otwayrees2.eva") (line (crypt (line (tuple (line "Na" 23 20 23 22 "otwayrees2.eva") (line "Kab" 23 24 23 27 "otwayrees2.eva")) 23 20 23 27 "otwayrees2.eva") (line "Kas" 23 29 23 32 "otwayrees2.eva") (vanilla)) 23 19 23 32 "otwayrees2.eva") (line (crypt (line (tuple (line "Nb" 23 35 23 37 "otwayrees2.eva") (line "Kab" 23 39 23 42 "otwayrees2.eva")) 23 35 23 42 "otwayrees2.eva") (line "Kbs" 23 44 23 47 "otwayrees2.eva") (vanilla)) 23 34 23 47 "otwayrees2.eva")) 23 16 23 47 "otwayrees2.eva")) 23 4 23 47 "otwayrees2.eva") (line (comm "4." (line "B" 24 7 24 8 "otwayrees2.eva") (line "A" 24 12 24 13 "otwayrees2.eva") (line (tuple (line "N" 24 16 24 17 "otwayrees2.eva") (line (crypt (line (tuple (line "Na" 24 20 24 22 "otwayrees2.eva") (line "Kab" 24 24 24 27 "otwayrees2.eva")) 24 20 24 27 "otwayrees2.eva") (line "Kas" 24 29 24 32 "otwayrees2.eva") (vanilla)) 24 19 24 32 "otwayrees2.eva")) 24 16 24 32 "otwayrees2.eva")) 24 4 24 32 "otwayrees2.eva")) 19 2 25 3 "otwayrees2.eva") 19 2 25 3 "otwayrees2.eva") (line (sessions (line (session-repeat (line (private (line "Kas" 27 16 27 19 "otwayrees2.eva") (line "Kbs" 27 21 27 24 "otwayrees2.eva")) 27 15 27 25 "otwayrees2.eva") "s1." (line (principals-except) 27 15 27 16 "otwayrees2.eva") (line (bind (line "A" 27 26 27 27 "otwayrees2.eva") (line "a" 27 28 27 29 "otwayrees2.eva")) 27 26 27 29 "otwayrees2.eva") (line (bind (line "B" 27 31 27 32 "otwayrees2.eva") (line "b" 27 33 27 34 "otwayrees2.eva")) 27 31 27 34 "otwayrees2.eva") (line (bind (line "S" 27 36 27 37 "otwayrees2.eva") (line "s" 27 38 27 39 "otwayrees2.eva")) 27 36 27 39 "otwayrees2.eva")) 27 2 27 39 "otwayrees2.eva")) 25 2 27 39 "") (line (assume (line (secret (line (locate "s1." (line "A" 29 24 29 25 "otwayrees2.eva") (line "Kas" 29 17 29 20 "otwayrees2.eva")) 29 17 29 25 "otwayrees2.eva")) 29 9 29 26 "otwayrees2.eva") (line (secret (line (locate "s1." (line "B" 29 43 29 44 "otwayrees2.eva") (line "Kbs" 29 36 29 39 "otwayrees2.eva")) 29 36 29 44 "otwayrees2.eva")) 29 28 29 45 "otwayrees2.eva") (line (prop (line "equals" 30 1 30 7 "otwayrees2.eva") (line (locate "s1." (line "A" 30 16 30 17 "otwayrees2.eva") (line "Kas" 30 9 30 12 "otwayrees2.eva")) 30 9 30 17 "otwayrees2.eva") (line (locate "s1." (line "S" 30 26 30 27 "otwayrees2.eva") (line "Kas" 30 19 30 22 "otwayrees2.eva")) 30 19 30 27 "otwayrees2.eva")) 30 1 30 28 "otwayrees2.eva") (line (prop (line "equals" 30 30 30 36 "otwayrees2.eva") (line (locate "s1." (line "B" 30 45 30 46 "otwayrees2.eva") (line "Kbs" 30 38 30 41 "otwayrees2.eva")) 30 38 30 46 "otwayrees2.eva") (line (locate "s1." (line "S" 30 55 30 56 "otwayrees2.eva") (line "Kbs" 30 48 30 51 "otwayrees2.eva")) 30 48 30 56 "otwayrees2.eva")) 30 30 30 57 "otwayrees2.eva")) 29 2 30 57 "otwayrees2.eva") (line (claim (line (A (line (G (line (secret (line (locate "s1." (line "A" 31 28 31 29 "otwayrees2.eva") (line "Kas" 31 21 31 24 "otwayrees2.eva")) 31 21 31 29 "otwayrees2.eva")) 31 13 31 30 "otwayrees2.eva")) 31 10 31 30 "otwayrees2.eva")) 31 8 31 30 "otwayrees2.eva") (line (A (line (G (line (secret (line (locate "s1." (line "B" 32 21 32 22 "otwayrees2.eva") (line "Kbs" 32 14 32 17 "otwayrees2.eva")) 32 14 32 22 "otwayrees2.eva")) 32 6 32 23 "otwayrees2.eva")) 32 3 32 23 "otwayrees2.eva")) 32 1 32 23 "otwayrees2.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 33 21 33 22 "otwayrees2.eva") (line "Kas" 33 14 33 17 "otwayrees2.eva")) 33 14 33 22 "otwayrees2.eva")) 33 6 33 23 "otwayrees2.eva")) 33 3 33 23 "otwayrees2.eva")) 33 1 33 23 "otwayrees2.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 34 21 34 22 "otwayrees2.eva") (line "Kbs" 34 14 34 17 "otwayrees2.eva")) 34 14 34 22 "otwayrees2.eva")) 34 6 34 23 "otwayrees2.eva")) 34 3 34 23 "otwayrees2.eva")) 34 1 34 23 "otwayrees2.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 35 21 35 22 "otwayrees2.eva") (line "Kab" 35 14 35 17 "otwayrees2.eva")) 35 14 35 22 "otwayrees2.eva")) 35 6 35 23 "otwayrees2.eva")) 35 3 35 23 "otwayrees2.eva")) 35 1 35 23 "otwayrees2.eva")) 31 2 35 23 "otwayrees2.eva")) 1 0 30 57 "otwayrees2.eva")