Terminals which are not used: kw_int kw_string_constant Conflict in state 121 between rule 91 and token kw_implies resolved as reduce. Conflict in state 121 between rule 91 and token kw_or resolved as reduce. Conflict in state 121 between rule 91 and token kw_U resolved as reduce. Conflict in state 121 between rule 91 and token kw_W resolved as reduce. Conflict in state 121 between rule 91 and token kw_S resolved as reduce. Conflict in state 121 between rule 91 and token kw_B resolved as reduce. Conflict in state 121 between rule 91 and token kw_and resolved as reduce. Conflict in state 122 between rule 93 and token kw_implies resolved as reduce. Conflict in state 122 between rule 93 and token kw_or resolved as reduce. Conflict in state 122 between rule 93 and token kw_U resolved as reduce. Conflict in state 122 between rule 93 and token kw_W resolved as reduce. Conflict in state 122 between rule 93 and token kw_S resolved as reduce. Conflict in state 122 between rule 93 and token kw_B resolved as reduce. Conflict in state 122 between rule 93 and token kw_and resolved as reduce. Conflict in state 123 between rule 94 and token kw_implies resolved as reduce. Conflict in state 123 between rule 94 and token kw_or resolved as reduce. Conflict in state 123 between rule 94 and token kw_U resolved as reduce. Conflict in state 123 between rule 94 and token kw_W resolved as reduce. Conflict in state 123 between rule 94 and token kw_S resolved as reduce. Conflict in state 123 between rule 94 and token kw_B resolved as reduce. Conflict in state 123 between rule 94 and token kw_and resolved as reduce. Conflict in state 124 between rule 96 and token kw_implies resolved as reduce. Conflict in state 124 between rule 96 and token kw_or resolved as reduce. Conflict in state 124 between rule 96 and token kw_U resolved as reduce. Conflict in state 124 between rule 96 and token kw_W resolved as reduce. Conflict in state 124 between rule 96 and token kw_S resolved as reduce. Conflict in state 124 between rule 96 and token kw_B resolved as reduce. Conflict in state 124 between rule 96 and token kw_and resolved as reduce. Conflict in state 125 between rule 97 and token kw_implies resolved as reduce. Conflict in state 125 between rule 97 and token kw_or resolved as reduce. Conflict in state 125 between rule 97 and token kw_U resolved as reduce. Conflict in state 125 between rule 97 and token kw_W resolved as reduce. Conflict in state 125 between rule 97 and token kw_S resolved as reduce. Conflict in state 125 between rule 97 and token kw_B resolved as reduce. Conflict in state 125 between rule 97 and token kw_and resolved as reduce. Conflict in state 126 between rule 98 and token kw_implies resolved as reduce. Conflict in state 126 between rule 98 and token kw_or resolved as reduce. Conflict in state 126 between rule 98 and token kw_U resolved as reduce. Conflict in state 126 between rule 98 and token kw_W resolved as reduce. Conflict in state 126 between rule 98 and token kw_S resolved as reduce. Conflict in state 126 between rule 98 and token kw_B resolved as reduce. Conflict in state 126 between rule 98 and token kw_and resolved as reduce. Conflict in state 127 between rule 99 and token kw_implies resolved as reduce. Conflict in state 127 between rule 99 and token kw_or resolved as reduce. Conflict in state 127 between rule 99 and token kw_U resolved as reduce. Conflict in state 127 between rule 99 and token kw_W resolved as reduce. Conflict in state 127 between rule 99 and token kw_S resolved as reduce. Conflict in state 127 between rule 99 and token kw_B resolved as reduce. Conflict in state 127 between rule 99 and token kw_and resolved as reduce. Conflict in state 128 between rule 95 and token kw_implies resolved as reduce. Conflict in state 128 between rule 95 and token kw_or resolved as reduce. Conflict in state 128 between rule 95 and token kw_U resolved as reduce. Conflict in state 128 between rule 95 and token kw_W resolved as reduce. Conflict in state 128 between rule 95 and token kw_S resolved as reduce. Conflict in state 128 between rule 95 and token kw_B resolved as reduce. Conflict in state 128 between rule 95 and token kw_and resolved as reduce. Conflict in state 165 between rule 90 and token kw_implies resolved as shift. Conflict in state 165 between rule 90 and token kw_or resolved as shift. Conflict in state 165 between rule 90 and token kw_U resolved as shift. Conflict in state 165 between rule 90 and token kw_W resolved as shift. Conflict in state 165 between rule 90 and token kw_S resolved as shift. Conflict in state 165 between rule 90 and token kw_B resolved as shift. Conflict in state 165 between rule 90 and token kw_and resolved as shift. Conflict in state 166 between rule 88 and token kw_implies resolved as reduce. Conflict in state 166 between rule 88 and token kw_or resolved as shift. Conflict in state 166 between rule 88 and token kw_U resolved as shift. Conflict in state 166 between rule 88 and token kw_W resolved as shift. Conflict in state 166 between rule 88 and token kw_S resolved as shift. Conflict in state 166 between rule 88 and token kw_B resolved as shift. Conflict in state 166 between rule 88 and token kw_and resolved as shift. Conflict in state 167 between rule 100 and token kw_implies resolved as reduce. Conflict in state 167 between rule 100 and token kw_or resolved as shift. Conflict in state 167 between rule 100 and token kw_U resolved as shift. Conflict in state 167 between rule 100 and token kw_W resolved as shift. Conflict in state 167 between rule 100 and token kw_S resolved as shift. Conflict in state 167 between rule 100 and token kw_B resolved as shift. Conflict in state 167 between rule 100 and token kw_and resolved as shift. Conflict in state 168 between rule 101 and token kw_implies resolved as reduce. Conflict in state 168 between rule 101 and token kw_or resolved as shift. Conflict in state 168 between rule 101 and token kw_U resolved as shift. Conflict in state 168 between rule 101 and token kw_W resolved as shift. Conflict in state 168 between rule 101 and token kw_S resolved as shift. Conflict in state 168 between rule 101 and token kw_B resolved as shift. Conflict in state 168 between rule 101 and token kw_and resolved as shift. Conflict in state 169 between rule 102 and token kw_implies resolved as reduce. Conflict in state 169 between rule 102 and token kw_or resolved as shift. Conflict in state 169 between rule 102 and token kw_U resolved as shift. Conflict in state 169 between rule 102 and token kw_W resolved as shift. Conflict in state 169 between rule 102 and token kw_S resolved as shift. Conflict in state 169 between rule 102 and token kw_B resolved as shift. Conflict in state 169 between rule 102 and token kw_and resolved as shift. Conflict in state 170 between rule 103 and token kw_implies resolved as reduce. Conflict in state 170 between rule 103 and token kw_or resolved as shift. Conflict in state 170 between rule 103 and token kw_U resolved as shift. Conflict in state 170 between rule 103 and token kw_W resolved as shift. Conflict in state 170 between rule 103 and token kw_S resolved as shift. Conflict in state 170 between rule 103 and token kw_B resolved as shift. Conflict in state 170 between rule 103 and token kw_and resolved as shift. Conflict in state 171 between rule 86 and token kw_implies resolved as reduce. Conflict in state 171 between rule 86 and token kw_or resolved as reduce. Conflict in state 171 between rule 86 and token kw_U resolved as reduce. Conflict in state 171 between rule 86 and token kw_W resolved as reduce. Conflict in state 171 between rule 86 and token kw_S resolved as reduce. Conflict in state 171 between rule 86 and token kw_B resolved as reduce. Conflict in state 171 between rule 86 and token kw_and resolved as shift. Grammar rule 1 spec -> id declarations block environment assumptions claims kw_eof rule 2 id -> kw_id rule 3 declarations -> /* empty */ rule 4 declarations -> declarations declaration rule 5 declaration -> typing_declaration rule 6 declaration -> kw_keypair optional_encryption_algorithm id ',' id optional_type_list rule 7 declaration -> kw_alias id '=' term rule 8 declaration -> ids ':' kw_alias id '=' term rule 9 declaration -> kw_basetype id rule 10 declaration -> kw_everybody kw_knows tuple rule 11 declaration -> id kw_knows tuple rule 12 declaration -> kw_axiom term '=' term optional_quantification rule 13 optional_quantification -> /* empty */ rule 14 optional_quantification -> '[' typing_declarations ']' rule 15 typing_declarations -> typing_declaration rule 16 typing_declarations -> typing_declarations ',' typing_declaration rule 17 typing_declaration -> ids ':' type optional_shared rule 18 typing_declaration -> id '(' type_list ')' ':' type optional_hash_or_secret rule 19 optional_shared -> /* empty */ rule 20 optional_shared -> kw_shared rule 21 optional_type_list -> '(' type_list ')' rule 22 optional_type_list -> /* empty */ rule 23 ids -> id rule 24 ids -> ids ',' id rule 25 type -> id rule 26 type_list -> /* empty */ rule 27 type_list -> non_empty_type_list rule 28 non_empty_type_list -> type rule 29 non_empty_type_list -> non_empty_type_list ',' type rule 30 optional_hash_or_secret -> optional_hash_or_secret kw_hash rule 31 optional_hash_or_secret -> optional_hash_or_secret kw_secret rule 32 optional_hash_or_secret -> /* empty */ rule 33 block -> '{' messages '}' rule 34 messages -> /* empty */ rule 35 messages -> messages message rule 36 message -> label id kw_arrow id ':' term rule 37 message -> id ':' id equals_or_assign_operator atomic_term_or_ciphertext rule 38 message -> block rule 39 message -> kw_switch term '{' cases '}' rule 40 label -> kw_label rule 41 equals_or_assign_operator -> kw_tst_equal rule 42 equals_or_assign_operator -> kw_assign rule 43 cases -> /* empty */ rule 44 cases -> cases case rule 45 case -> kw_case term ':' messages rule 46 term -> tuple rule 47 tuple -> atomic_term_or_ciphertext rule 48 tuple -> tuple ',' atomic_term_or_ciphertext rule 49 term_list -> '(' ')' rule 50 term_list -> '(' tuple ')' rule 51 atomic_term_or_ciphertext -> atomic_term rule 52 atomic_term_or_ciphertext -> '{' term '}' '_' atomic_term optional_encryption_algorithm rule 53 atomic_term_or_ciphertext -> '{' term '}' '^' atomic_term '_' atomic_term rule 54 atomic_term_or_ciphertext -> '[' term ']' '_' atomic_term optional_encryption_algorithm rule 55 atomic_term_or_ciphertext -> atomic_term '%' atomic_term rule 56 atomic_term_or_ciphertext -> atomic_term_or_ciphertext '@' label id rule 57 atomic_term -> id term_list rule 58 atomic_term -> id rule 59 atomic_term -> '(' term ')' rule 60 atomic_term -> '(' ')' rule 61 optional_encryption_algorithm -> /* empty */ rule 62 optional_encryption_algorithm -> '^' atomic_term rule 63 environment -> /* empty */ rule 64 environment -> environment session rule 65 session -> optional_label kw_session optional_repeat principals assignments rule 66 optional_label -> label rule 67 optional_label -> /* empty */ rule 68 optional_repeat -> /* empty */ rule 69 optional_repeat -> '*' '{' ids '}' rule 70 assignments -> assignment rule 71 assignments -> assignments ',' assignment rule 72 assignment -> id '=' atomic_term_or_ciphertext rule 73 principals -> '[' ids ']' rule 74 principals -> '[' '^' ids ']' rule 75 principals -> /* empty */ rule 76 assumptions -> kw_assume properties rule 77 assumptions -> /* empty */ rule 78 claims -> kw_claim properties rule 79 claims -> /* empty */ rule 80 properties -> property rule 81 properties -> properties ',' property rule 82 property -> id term_list rule 83 property -> label id '@' label rule 84 property -> label id '(' term ')' rule 85 property -> kw_secret '(' term ')' rule 86 property -> property kw_and property rule 87 property -> kw_true rule 88 property -> property kw_or property rule 89 property -> kw_false rule 90 property -> property kw_implies property rule 91 property -> '!' property rule 92 property -> '(' property ')' rule 93 property -> kw_E property rule 94 property -> kw_A property rule 95 property -> kw_N property rule 96 property -> kw_F property rule 97 property -> kw_G property rule 98 property -> kw_P property rule 99 property -> kw_Q property rule 100 property -> property kw_U property rule 101 property -> property kw_W property rule 102 property -> property kw_S property rule 103 property -> property kw_B property Terminals, with rules where they appear $ (-1) '!' (33) 91 '%' (37) 55 '(' (40) 18 21 49 50 59 60 84 85 92 ')' (41) 18 21 49 50 59 60 84 85 92 '*' (42) 69 ',' (44) 6 16 24 29 48 71 81 ':' (58) 8 17 18 36 37 45 '=' (61) 7 8 12 72 '@' (64) 56 83 '[' (91) 14 54 73 74 ']' (93) 14 54 73 74 '^' (94) 53 62 74 '_' (95) 52 53 54 '{' (123) 33 39 52 53 69 '}' (125) 33 39 52 53 69 error (256) kw_int (257) kw_id (258) 2 kw_label (259) 40 kw_alias (260) 7 8 kw_axiom (261) 12 kw_basetype (262) 9 kw_case (263) 45 kw_everybody (264) 10 kw_hash (265) 30 kw_knows (266) 10 11 kw_session (267) 65 kw_secret (268) 31 85 kw_switch (269) 39 kw_arrow (270) 36 kw_assign (271) 42 kw_eof (272) 1 kw_string_constant (273) kw_keypair (274) 6 kw_assume (275) 76 kw_claim (276) 78 kw_tst_equal (277) 41 kw_true (278) 87 kw_false (279) 89 kw_shared (280) 20 kw_implies (281) 90 kw_or (282) 88 kw_U (283) 100 kw_W (284) 101 kw_S (285) 102 kw_B (286) 103 kw_and (287) 86 kw_E (288) 93 kw_A (289) 94 kw_F (290) 96 kw_G (291) 97 kw_P (292) 98 kw_Q (293) 99 kw_N (294) 95 Nonterminals, with rules where they appear spec (56) on left: 1 id (57) on left: 2, on right: 1 6 7 8 9 11 18 23 24 25 36 37 56 57 58 72 82 83 84 declarations (58) on left: 3 4, on right: 1 4 declaration (59) on left: 5 6 7 8 9 10 11 12, on right: 4 optional_quantification (60) on left: 13 14, on right: 12 typing_declarations (61) on left: 15 16, on right: 14 16 typing_declaration (62) on left: 17 18, on right: 5 15 16 optional_shared (63) on left: 19 20, on right: 17 optional_type_list (64) on left: 21 22, on right: 6 ids (65) on left: 23 24, on right: 8 17 24 69 73 74 type (66) on left: 25, on right: 17 18 28 29 type_list (67) on left: 26 27, on right: 18 21 non_empty_type_list (68) on left: 28 29, on right: 27 29 optional_hash_or_secret (69) on left: 30 31 32, on right: 18 30 31 block (70) on left: 33, on right: 1 38 messages (71) on left: 34 35, on right: 33 35 45 message (72) on left: 36 37 38 39, on right: 35 label (73) on left: 40, on right: 36 56 66 83 84 equals_or_assign_operator (74) on left: 41 42, on right: 37 cases (75) on left: 43 44, on right: 39 44 case (76) on left: 45, on right: 44 term (77) on left: 46, on right: 7 8 12 36 39 45 52 53 54 59 84 85 tuple (78) on left: 47 48, on right: 10 11 46 48 50 term_list (79) on left: 49 50, on right: 57 82 atomic_term_or_ciphertext (80) on left: 51 52 53 54 55 56, on right: 37 47 48 56 72 atomic_term (81) on left: 57 58 59 60, on right: 51 52 53 54 55 62 optional_encryption_algorithm (82) on left: 61 62, on right: 6 52 54 environment (83) on left: 63 64, on right: 1 64 session (84) on left: 65, on right: 64 optional_label (85) on left: 66 67, on right: 65 optional_repeat (86) on left: 68 69, on right: 65 assignments (87) on left: 70 71, on right: 65 71 assignment (88) on left: 72, on right: 70 71 principals (89) on left: 73 74 75, on right: 65 assumptions (90) on left: 76 77, on right: 1 claims (91) on left: 78 79, on right: 1 properties (92) on left: 80 81, on right: 76 78 81 property (93) on left: 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103, on right: 80 81 86 88 90 91 92 93 94 95 96 97 98 99 100 101 102 103 state 0 kw_id shift, and go to state 1 spec go to state 216 id go to state 2 state 1 id -> kw_id . (rule 2) $default reduce using rule 2 (id) state 2 spec -> id . declarations block environment assumptions claims kw_eof (rule 1) $default reduce using rule 3 (declarations) declarations go to state 3 state 3 spec -> id declarations . block environment assumptions claims kw_eof (rule 1) declarations -> declarations . declaration (rule 4) kw_id shift, and go to state 1 kw_alias shift, and go to state 4 kw_axiom shift, and go to state 5 kw_basetype shift, and go to state 6 kw_everybody shift, and go to state 7 kw_keypair shift, and go to state 8 '{' shift, and go to state 9 id go to state 10 declaration go to state 11 typing_declaration go to state 12 ids go to state 13 block go to state 14 state 4 declaration -> kw_alias . id '=' term (rule 7) kw_id shift, and go to state 1 id go to state 15 state 5 declaration -> kw_axiom . term '=' term optional_quantification (rule 12) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 20 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 6 declaration -> kw_basetype . id (rule 9) kw_id shift, and go to state 1 id go to state 24 state 7 declaration -> kw_everybody . kw_knows tuple (rule 10) kw_knows shift, and go to state 25 state 8 declaration -> kw_keypair . optional_encryption_algorithm id ',' id optional_type_list (rule 6) '^' shift, and go to state 26 $default reduce using rule 61 (optional_encryption_algorithm) optional_encryption_algorithm go to state 27 state 9 block -> '{' . messages '}' (rule 33) $default reduce using rule 34 (messages) messages go to state 28 state 10 declaration -> id . kw_knows tuple (rule 11) typing_declaration -> id . '(' type_list ')' ':' type optional_hash_or_secret (rule 18) ids -> id . (rule 23) kw_knows shift, and go to state 29 '(' shift, and go to state 30 $default reduce using rule 23 (ids) state 11 declarations -> declarations declaration . (rule 4) $default reduce using rule 4 (declarations) state 12 declaration -> typing_declaration . (rule 5) $default reduce using rule 5 (declaration) state 13 declaration -> ids . ':' kw_alias id '=' term (rule 8) typing_declaration -> ids . ':' type optional_shared (rule 17) ids -> ids . ',' id (rule 24) ',' shift, and go to state 31 ':' shift, and go to state 32 state 14 spec -> id declarations block . environment assumptions claims kw_eof (rule 1) $default reduce using rule 63 (environment) environment go to state 33 state 15 declaration -> kw_alias id . '=' term (rule 7) '=' shift, and go to state 34 state 16 atomic_term_or_ciphertext -> '[' . term ']' '_' atomic_term optional_encryption_algorithm (rule 54) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 35 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 17 atomic_term -> '(' . term ')' (rule 59) atomic_term -> '(' . ')' (rule 60) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 ')' shift, and go to state 36 '{' shift, and go to state 18 id go to state 19 term go to state 37 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 18 atomic_term_or_ciphertext -> '{' . term '}' '_' atomic_term optional_encryption_algorithm (rule 52) atomic_term_or_ciphertext -> '{' . term '}' '^' atomic_term '_' atomic_term (rule 53) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 38 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 19 atomic_term -> id . term_list (rule 57) atomic_term -> id . (rule 58) '(' shift, and go to state 39 $default reduce using rule 58 (atomic_term) term_list go to state 40 state 20 declaration -> kw_axiom term . '=' term optional_quantification (rule 12) '=' shift, and go to state 41 state 21 term -> tuple . (rule 46) tuple -> tuple . ',' atomic_term_or_ciphertext (rule 48) ',' shift, and go to state 42 $default reduce using rule 46 (term) state 22 tuple -> atomic_term_or_ciphertext . (rule 47) atomic_term_or_ciphertext -> atomic_term_or_ciphertext . '@' label id (rule 56) '@' shift, and go to state 43 $default reduce using rule 47 (tuple) state 23 atomic_term_or_ciphertext -> atomic_term . (rule 51) atomic_term_or_ciphertext -> atomic_term . '%' atomic_term (rule 55) '%' shift, and go to state 44 $default reduce using rule 51 (atomic_term_or_ciphertext) state 24 declaration -> kw_basetype id . (rule 9) $default reduce using rule 9 (declaration) state 25 declaration -> kw_everybody kw_knows . tuple (rule 10) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 tuple go to state 45 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 26 optional_encryption_algorithm -> '^' . atomic_term (rule 62) kw_id shift, and go to state 1 '(' shift, and go to state 17 id go to state 19 atomic_term go to state 46 state 27 declaration -> kw_keypair optional_encryption_algorithm . id ',' id optional_type_list (rule 6) kw_id shift, and go to state 1 id go to state 47 state 28 block -> '{' messages . '}' (rule 33) messages -> messages . message (rule 35) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_switch shift, and go to state 49 '{' shift, and go to state 9 '}' shift, and go to state 50 id go to state 51 block go to state 52 message go to state 53 label go to state 54 state 29 declaration -> id kw_knows . tuple (rule 11) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 tuple go to state 55 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 30 typing_declaration -> id '(' . type_list ')' ':' type optional_hash_or_secret (rule 18) kw_id shift, and go to state 1 $default reduce using rule 26 (type_list) id go to state 56 type go to state 57 type_list go to state 58 non_empty_type_list go to state 59 state 31 ids -> ids ',' . id (rule 24) kw_id shift, and go to state 1 id go to state 60 state 32 declaration -> ids ':' . kw_alias id '=' term (rule 8) typing_declaration -> ids ':' . type optional_shared (rule 17) kw_id shift, and go to state 1 kw_alias shift, and go to state 61 id go to state 56 type go to state 62 state 33 spec -> id declarations block environment . assumptions claims kw_eof (rule 1) environment -> environment . session (rule 64) kw_label shift, and go to state 48 kw_assume shift, and go to state 63 kw_session reduce using rule 67 (optional_label) $default reduce using rule 77 (assumptions) label go to state 64 session go to state 65 optional_label go to state 66 assumptions go to state 67 state 34 declaration -> kw_alias id '=' . term (rule 7) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 68 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 35 atomic_term_or_ciphertext -> '[' term . ']' '_' atomic_term optional_encryption_algorithm (rule 54) ']' shift, and go to state 69 state 36 atomic_term -> '(' ')' . (rule 60) $default reduce using rule 60 (atomic_term) state 37 atomic_term -> '(' term . ')' (rule 59) ')' shift, and go to state 70 state 38 atomic_term_or_ciphertext -> '{' term . '}' '_' atomic_term optional_encryption_algorithm (rule 52) atomic_term_or_ciphertext -> '{' term . '}' '^' atomic_term '_' atomic_term (rule 53) '}' shift, and go to state 71 state 39 term_list -> '(' . ')' (rule 49) term_list -> '(' . tuple ')' (rule 50) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 ')' shift, and go to state 72 '{' shift, and go to state 18 id go to state 19 tuple go to state 73 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 40 atomic_term -> id term_list . (rule 57) $default reduce using rule 57 (atomic_term) state 41 declaration -> kw_axiom term '=' . term optional_quantification (rule 12) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 74 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 42 tuple -> tuple ',' . atomic_term_or_ciphertext (rule 48) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 atomic_term_or_ciphertext go to state 75 atomic_term go to state 23 state 43 atomic_term_or_ciphertext -> atomic_term_or_ciphertext '@' . label id (rule 56) kw_label shift, and go to state 48 label go to state 76 state 44 atomic_term_or_ciphertext -> atomic_term '%' . atomic_term (rule 55) kw_id shift, and go to state 1 '(' shift, and go to state 17 id go to state 19 atomic_term go to state 77 state 45 declaration -> kw_everybody kw_knows tuple . (rule 10) tuple -> tuple . ',' atomic_term_or_ciphertext (rule 48) ',' shift, and go to state 42 $default reduce using rule 10 (declaration) state 46 optional_encryption_algorithm -> '^' atomic_term . (rule 62) $default reduce using rule 62 (optional_encryption_algorithm) state 47 declaration -> kw_keypair optional_encryption_algorithm id . ',' id optional_type_list (rule 6) ',' shift, and go to state 78 state 48 label -> kw_label . (rule 40) $default reduce using rule 40 (label) state 49 message -> kw_switch . term '{' cases '}' (rule 39) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 79 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 50 block -> '{' messages '}' . (rule 33) $default reduce using rule 33 (block) state 51 message -> id . ':' id equals_or_assign_operator atomic_term_or_ciphertext (rule 37) ':' shift, and go to state 80 state 52 message -> block . (rule 38) $default reduce using rule 38 (message) state 53 messages -> messages message . (rule 35) $default reduce using rule 35 (messages) state 54 message -> label . id kw_arrow id ':' term (rule 36) kw_id shift, and go to state 1 id go to state 81 state 55 declaration -> id kw_knows tuple . (rule 11) tuple -> tuple . ',' atomic_term_or_ciphertext (rule 48) ',' shift, and go to state 42 $default reduce using rule 11 (declaration) state 56 type -> id . (rule 25) $default reduce using rule 25 (type) state 57 non_empty_type_list -> type . (rule 28) $default reduce using rule 28 (non_empty_type_list) state 58 typing_declaration -> id '(' type_list . ')' ':' type optional_hash_or_secret (rule 18) ')' shift, and go to state 82 state 59 type_list -> non_empty_type_list . (rule 27) non_empty_type_list -> non_empty_type_list . ',' type (rule 29) ',' shift, and go to state 83 $default reduce using rule 27 (type_list) state 60 ids -> ids ',' id . (rule 24) $default reduce using rule 24 (ids) state 61 declaration -> ids ':' kw_alias . id '=' term (rule 8) kw_id shift, and go to state 1 id go to state 84 state 62 typing_declaration -> ids ':' type . optional_shared (rule 17) kw_shared shift, and go to state 85 $default reduce using rule 19 (optional_shared) optional_shared go to state 86 state 63 assumptions -> kw_assume . properties (rule 76) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 properties go to state 101 property go to state 102 state 64 optional_label -> label . (rule 66) $default reduce using rule 66 (optional_label) state 65 environment -> environment session . (rule 64) $default reduce using rule 64 (environment) state 66 session -> optional_label . kw_session optional_repeat principals assignments (rule 65) kw_session shift, and go to state 103 state 67 spec -> id declarations block environment assumptions . claims kw_eof (rule 1) kw_claim shift, and go to state 104 $default reduce using rule 79 (claims) claims go to state 105 state 68 declaration -> kw_alias id '=' term . (rule 7) $default reduce using rule 7 (declaration) state 69 atomic_term_or_ciphertext -> '[' term ']' . '_' atomic_term optional_encryption_algorithm (rule 54) '_' shift, and go to state 106 state 70 atomic_term -> '(' term ')' . (rule 59) $default reduce using rule 59 (atomic_term) state 71 atomic_term_or_ciphertext -> '{' term '}' . '_' atomic_term optional_encryption_algorithm (rule 52) atomic_term_or_ciphertext -> '{' term '}' . '^' atomic_term '_' atomic_term (rule 53) '_' shift, and go to state 107 '^' shift, and go to state 108 state 72 term_list -> '(' ')' . (rule 49) $default reduce using rule 49 (term_list) state 73 tuple -> tuple . ',' atomic_term_or_ciphertext (rule 48) term_list -> '(' tuple . ')' (rule 50) ',' shift, and go to state 42 ')' shift, and go to state 109 state 74 declaration -> kw_axiom term '=' term . optional_quantification (rule 12) '[' shift, and go to state 110 $default reduce using rule 13 (optional_quantification) optional_quantification go to state 111 state 75 tuple -> tuple ',' atomic_term_or_ciphertext . (rule 48) atomic_term_or_ciphertext -> atomic_term_or_ciphertext . '@' label id (rule 56) '@' shift, and go to state 43 $default reduce using rule 48 (tuple) state 76 atomic_term_or_ciphertext -> atomic_term_or_ciphertext '@' label . id (rule 56) kw_id shift, and go to state 1 id go to state 112 state 77 atomic_term_or_ciphertext -> atomic_term '%' atomic_term . (rule 55) $default reduce using rule 55 (atomic_term_or_ciphertext) state 78 declaration -> kw_keypair optional_encryption_algorithm id ',' . id optional_type_list (rule 6) kw_id shift, and go to state 1 id go to state 113 state 79 message -> kw_switch term . '{' cases '}' (rule 39) '{' shift, and go to state 114 state 80 message -> id ':' . id equals_or_assign_operator atomic_term_or_ciphertext (rule 37) kw_id shift, and go to state 1 id go to state 115 state 81 message -> label id . kw_arrow id ':' term (rule 36) kw_arrow shift, and go to state 116 state 82 typing_declaration -> id '(' type_list ')' . ':' type optional_hash_or_secret (rule 18) ':' shift, and go to state 117 state 83 non_empty_type_list -> non_empty_type_list ',' . type (rule 29) kw_id shift, and go to state 1 id go to state 56 type go to state 118 state 84 declaration -> ids ':' kw_alias id . '=' term (rule 8) '=' shift, and go to state 119 state 85 optional_shared -> kw_shared . (rule 20) $default reduce using rule 20 (optional_shared) state 86 typing_declaration -> ids ':' type optional_shared . (rule 17) $default reduce using rule 17 (typing_declaration) state 87 property -> kw_secret . '(' term ')' (rule 85) '(' shift, and go to state 120 state 88 property -> kw_true . (rule 87) $default reduce using rule 87 (property) state 89 property -> kw_false . (rule 89) $default reduce using rule 89 (property) state 90 property -> '!' . property (rule 91) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 121 state 91 property -> kw_E . property (rule 93) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 122 state 92 property -> kw_A . property (rule 94) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 123 state 93 property -> kw_F . property (rule 96) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 124 state 94 property -> kw_G . property (rule 97) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 125 state 95 property -> kw_P . property (rule 98) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 126 state 96 property -> kw_Q . property (rule 99) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 127 state 97 property -> kw_N . property (rule 95) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 128 state 98 property -> '(' . property ')' (rule 92) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 129 state 99 property -> id . term_list (rule 82) '(' shift, and go to state 39 term_list go to state 130 state 100 property -> label . id '@' label (rule 83) property -> label . id '(' term ')' (rule 84) kw_id shift, and go to state 1 id go to state 131 state 101 assumptions -> kw_assume properties . (rule 76) properties -> properties . ',' property (rule 81) ',' shift, and go to state 132 $default reduce using rule 76 (assumptions) state 102 properties -> property . (rule 80) property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_implies shift, and go to state 133 kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 80 (properties) state 103 session -> optional_label kw_session . optional_repeat principals assignments (rule 65) '*' shift, and go to state 140 $default reduce using rule 68 (optional_repeat) optional_repeat go to state 141 state 104 claims -> kw_claim . properties (rule 78) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 properties go to state 142 property go to state 102 state 105 spec -> id declarations block environment assumptions claims . kw_eof (rule 1) kw_eof shift, and go to state 143 state 106 atomic_term_or_ciphertext -> '[' term ']' '_' . atomic_term optional_encryption_algorithm (rule 54) kw_id shift, and go to state 1 '(' shift, and go to state 17 id go to state 19 atomic_term go to state 144 state 107 atomic_term_or_ciphertext -> '{' term '}' '_' . atomic_term optional_encryption_algorithm (rule 52) kw_id shift, and go to state 1 '(' shift, and go to state 17 id go to state 19 atomic_term go to state 145 state 108 atomic_term_or_ciphertext -> '{' term '}' '^' . atomic_term '_' atomic_term (rule 53) kw_id shift, and go to state 1 '(' shift, and go to state 17 id go to state 19 atomic_term go to state 146 state 109 term_list -> '(' tuple ')' . (rule 50) $default reduce using rule 50 (term_list) state 110 optional_quantification -> '[' . typing_declarations ']' (rule 14) kw_id shift, and go to state 1 id go to state 147 typing_declarations go to state 148 typing_declaration go to state 149 ids go to state 150 state 111 declaration -> kw_axiom term '=' term optional_quantification . (rule 12) $default reduce using rule 12 (declaration) state 112 atomic_term_or_ciphertext -> atomic_term_or_ciphertext '@' label id . (rule 56) $default reduce using rule 56 (atomic_term_or_ciphertext) state 113 declaration -> kw_keypair optional_encryption_algorithm id ',' id . optional_type_list (rule 6) '(' shift, and go to state 151 $default reduce using rule 22 (optional_type_list) optional_type_list go to state 152 state 114 message -> kw_switch term '{' . cases '}' (rule 39) $default reduce using rule 43 (cases) cases go to state 153 state 115 message -> id ':' id . equals_or_assign_operator atomic_term_or_ciphertext (rule 37) kw_assign shift, and go to state 154 kw_tst_equal shift, and go to state 155 equals_or_assign_operator go to state 156 state 116 message -> label id kw_arrow . id ':' term (rule 36) kw_id shift, and go to state 1 id go to state 157 state 117 typing_declaration -> id '(' type_list ')' ':' . type optional_hash_or_secret (rule 18) kw_id shift, and go to state 1 id go to state 56 type go to state 158 state 118 non_empty_type_list -> non_empty_type_list ',' type . (rule 29) $default reduce using rule 29 (non_empty_type_list) state 119 declaration -> ids ':' kw_alias id '=' . term (rule 8) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 159 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 120 property -> kw_secret '(' . term ')' (rule 85) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 160 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 121 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> '!' property . (rule 91) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 91 (property) state 122 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_E property . (rule 93) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 93 (property) state 123 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_A property . (rule 94) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 94 (property) state 124 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_F property . (rule 96) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 96 (property) state 125 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_G property . (rule 97) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 97 (property) state 126 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_P property . (rule 98) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 98 (property) state 127 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_Q property . (rule 99) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 99 (property) state 128 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> kw_N property . (rule 95) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) $default reduce using rule 95 (property) state 129 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> '(' property . ')' (rule 92) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_implies shift, and go to state 133 kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 ')' shift, and go to state 161 state 130 property -> id term_list . (rule 82) $default reduce using rule 82 (property) state 131 property -> label id . '@' label (rule 83) property -> label id . '(' term ')' (rule 84) '(' shift, and go to state 162 '@' shift, and go to state 163 state 132 properties -> properties ',' . property (rule 81) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 164 state 133 property -> property kw_implies . property (rule 90) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 165 state 134 property -> property kw_or . property (rule 88) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 166 state 135 property -> property kw_U . property (rule 100) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 167 state 136 property -> property kw_W . property (rule 101) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 168 state 137 property -> property kw_S . property (rule 102) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 169 state 138 property -> property kw_B . property (rule 103) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 170 state 139 property -> property kw_and . property (rule 86) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_secret shift, and go to state 87 kw_true shift, and go to state 88 kw_false shift, and go to state 89 '!' shift, and go to state 90 kw_E shift, and go to state 91 kw_A shift, and go to state 92 kw_F shift, and go to state 93 kw_G shift, and go to state 94 kw_P shift, and go to state 95 kw_Q shift, and go to state 96 kw_N shift, and go to state 97 '(' shift, and go to state 98 id go to state 99 label go to state 100 property go to state 171 state 140 optional_repeat -> '*' . '{' ids '}' (rule 69) '{' shift, and go to state 172 state 141 session -> optional_label kw_session optional_repeat . principals assignments (rule 65) '[' shift, and go to state 173 $default reduce using rule 75 (principals) principals go to state 174 state 142 claims -> kw_claim properties . (rule 78) properties -> properties . ',' property (rule 81) ',' shift, and go to state 132 $default reduce using rule 78 (claims) state 143 spec -> id declarations block environment assumptions claims kw_eof . (rule 1) $default reduce using rule 1 (spec) state 144 atomic_term_or_ciphertext -> '[' term ']' '_' atomic_term . optional_encryption_algorithm (rule 54) '^' shift, and go to state 26 $default reduce using rule 61 (optional_encryption_algorithm) optional_encryption_algorithm go to state 175 state 145 atomic_term_or_ciphertext -> '{' term '}' '_' atomic_term . optional_encryption_algorithm (rule 52) '^' shift, and go to state 26 $default reduce using rule 61 (optional_encryption_algorithm) optional_encryption_algorithm go to state 176 state 146 atomic_term_or_ciphertext -> '{' term '}' '^' atomic_term . '_' atomic_term (rule 53) '_' shift, and go to state 177 state 147 typing_declaration -> id . '(' type_list ')' ':' type optional_hash_or_secret (rule 18) ids -> id . (rule 23) '(' shift, and go to state 30 $default reduce using rule 23 (ids) state 148 optional_quantification -> '[' typing_declarations . ']' (rule 14) typing_declarations -> typing_declarations . ',' typing_declaration (rule 16) ',' shift, and go to state 178 ']' shift, and go to state 179 state 149 typing_declarations -> typing_declaration . (rule 15) $default reduce using rule 15 (typing_declarations) state 150 typing_declaration -> ids . ':' type optional_shared (rule 17) ids -> ids . ',' id (rule 24) ',' shift, and go to state 31 ':' shift, and go to state 180 state 151 optional_type_list -> '(' . type_list ')' (rule 21) kw_id shift, and go to state 1 $default reduce using rule 26 (type_list) id go to state 56 type go to state 57 type_list go to state 181 non_empty_type_list go to state 59 state 152 declaration -> kw_keypair optional_encryption_algorithm id ',' id optional_type_list . (rule 6) $default reduce using rule 6 (declaration) state 153 message -> kw_switch term '{' cases . '}' (rule 39) cases -> cases . case (rule 44) kw_case shift, and go to state 182 '}' shift, and go to state 183 case go to state 184 state 154 equals_or_assign_operator -> kw_assign . (rule 42) $default reduce using rule 42 (equals_or_assign_operator) state 155 equals_or_assign_operator -> kw_tst_equal . (rule 41) $default reduce using rule 41 (equals_or_assign_operator) state 156 message -> id ':' id equals_or_assign_operator . atomic_term_or_ciphertext (rule 37) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 atomic_term_or_ciphertext go to state 185 atomic_term go to state 23 state 157 message -> label id kw_arrow id . ':' term (rule 36) ':' shift, and go to state 186 state 158 typing_declaration -> id '(' type_list ')' ':' type . optional_hash_or_secret (rule 18) $default reduce using rule 32 (optional_hash_or_secret) optional_hash_or_secret go to state 187 state 159 declaration -> ids ':' kw_alias id '=' term . (rule 8) $default reduce using rule 8 (declaration) state 160 property -> kw_secret '(' term . ')' (rule 85) ')' shift, and go to state 188 state 161 property -> '(' property ')' . (rule 92) $default reduce using rule 92 (property) state 162 property -> label id '(' . term ')' (rule 84) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 189 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 163 property -> label id '@' . label (rule 83) kw_label shift, and go to state 48 label go to state 190 state 164 properties -> properties ',' property . (rule 81) property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_implies shift, and go to state 133 kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 81 (properties) state 165 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property kw_implies property . (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_implies shift, and go to state 133 kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 90 (property) state 166 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property kw_or property . (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 88 (property) state 167 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property kw_U property . (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 100 (property) state 168 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property kw_W property . (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 101 (property) state 169 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property kw_S property . (rule 102) property -> property . kw_B property (rule 103) kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 102 (property) state 170 property -> property . kw_and property (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) property -> property kw_B property . (rule 103) kw_or shift, and go to state 134 kw_U shift, and go to state 135 kw_W shift, and go to state 136 kw_S shift, and go to state 137 kw_B shift, and go to state 138 kw_and shift, and go to state 139 $default reduce using rule 103 (property) state 171 property -> property . kw_and property (rule 86) property -> property kw_and property . (rule 86) property -> property . kw_or property (rule 88) property -> property . kw_implies property (rule 90) property -> property . kw_U property (rule 100) property -> property . kw_W property (rule 101) property -> property . kw_S property (rule 102) property -> property . kw_B property (rule 103) kw_and shift, and go to state 139 $default reduce using rule 86 (property) state 172 optional_repeat -> '*' '{' . ids '}' (rule 69) kw_id shift, and go to state 1 id go to state 191 ids go to state 192 state 173 principals -> '[' . ids ']' (rule 73) principals -> '[' . '^' ids ']' (rule 74) kw_id shift, and go to state 1 '^' shift, and go to state 193 id go to state 191 ids go to state 194 state 174 session -> optional_label kw_session optional_repeat principals . assignments (rule 65) kw_id shift, and go to state 1 id go to state 195 assignments go to state 196 assignment go to state 197 state 175 atomic_term_or_ciphertext -> '[' term ']' '_' atomic_term optional_encryption_algorithm . (rule 54) $default reduce using rule 54 (atomic_term_or_ciphertext) state 176 atomic_term_or_ciphertext -> '{' term '}' '_' atomic_term optional_encryption_algorithm . (rule 52) $default reduce using rule 52 (atomic_term_or_ciphertext) state 177 atomic_term_or_ciphertext -> '{' term '}' '^' atomic_term '_' . atomic_term (rule 53) kw_id shift, and go to state 1 '(' shift, and go to state 17 id go to state 19 atomic_term go to state 198 state 178 typing_declarations -> typing_declarations ',' . typing_declaration (rule 16) kw_id shift, and go to state 1 id go to state 147 typing_declaration go to state 199 ids go to state 150 state 179 optional_quantification -> '[' typing_declarations ']' . (rule 14) $default reduce using rule 14 (optional_quantification) state 180 typing_declaration -> ids ':' . type optional_shared (rule 17) kw_id shift, and go to state 1 id go to state 56 type go to state 62 state 181 optional_type_list -> '(' type_list . ')' (rule 21) ')' shift, and go to state 200 state 182 case -> kw_case . term ':' messages (rule 45) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 201 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 183 message -> kw_switch term '{' cases '}' . (rule 39) $default reduce using rule 39 (message) state 184 cases -> cases case . (rule 44) $default reduce using rule 44 (cases) state 185 message -> id ':' id equals_or_assign_operator atomic_term_or_ciphertext . (rule 37) atomic_term_or_ciphertext -> atomic_term_or_ciphertext . '@' label id (rule 56) '@' shift, and go to state 43 $default reduce using rule 37 (message) state 186 message -> label id kw_arrow id ':' . term (rule 36) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 term go to state 202 tuple go to state 21 atomic_term_or_ciphertext go to state 22 atomic_term go to state 23 state 187 typing_declaration -> id '(' type_list ')' ':' type optional_hash_or_secret . (rule 18) optional_hash_or_secret -> optional_hash_or_secret . kw_hash (rule 30) optional_hash_or_secret -> optional_hash_or_secret . kw_secret (rule 31) kw_hash shift, and go to state 203 kw_secret shift, and go to state 204 $default reduce using rule 18 (typing_declaration) state 188 property -> kw_secret '(' term ')' . (rule 85) $default reduce using rule 85 (property) state 189 property -> label id '(' term . ')' (rule 84) ')' shift, and go to state 205 state 190 property -> label id '@' label . (rule 83) $default reduce using rule 83 (property) state 191 ids -> id . (rule 23) $default reduce using rule 23 (ids) state 192 ids -> ids . ',' id (rule 24) optional_repeat -> '*' '{' ids . '}' (rule 69) ',' shift, and go to state 31 '}' shift, and go to state 206 state 193 principals -> '[' '^' . ids ']' (rule 74) kw_id shift, and go to state 1 id go to state 191 ids go to state 207 state 194 ids -> ids . ',' id (rule 24) principals -> '[' ids . ']' (rule 73) ',' shift, and go to state 31 ']' shift, and go to state 208 state 195 assignment -> id . '=' atomic_term_or_ciphertext (rule 72) '=' shift, and go to state 209 state 196 session -> optional_label kw_session optional_repeat principals assignments . (rule 65) assignments -> assignments . ',' assignment (rule 71) ',' shift, and go to state 210 $default reduce using rule 65 (session) state 197 assignments -> assignment . (rule 70) $default reduce using rule 70 (assignments) state 198 atomic_term_or_ciphertext -> '{' term '}' '^' atomic_term '_' atomic_term . (rule 53) $default reduce using rule 53 (atomic_term_or_ciphertext) state 199 typing_declarations -> typing_declarations ',' typing_declaration . (rule 16) $default reduce using rule 16 (typing_declarations) state 200 optional_type_list -> '(' type_list ')' . (rule 21) $default reduce using rule 21 (optional_type_list) state 201 case -> kw_case term . ':' messages (rule 45) ':' shift, and go to state 211 state 202 message -> label id kw_arrow id ':' term . (rule 36) $default reduce using rule 36 (message) state 203 optional_hash_or_secret -> optional_hash_or_secret kw_hash . (rule 30) $default reduce using rule 30 (optional_hash_or_secret) state 204 optional_hash_or_secret -> optional_hash_or_secret kw_secret . (rule 31) $default reduce using rule 31 (optional_hash_or_secret) state 205 property -> label id '(' term ')' . (rule 84) $default reduce using rule 84 (property) state 206 optional_repeat -> '*' '{' ids '}' . (rule 69) $default reduce using rule 69 (optional_repeat) state 207 ids -> ids . ',' id (rule 24) principals -> '[' '^' ids . ']' (rule 74) ',' shift, and go to state 31 ']' shift, and go to state 212 state 208 principals -> '[' ids ']' . (rule 73) $default reduce using rule 73 (principals) state 209 assignment -> id '=' . atomic_term_or_ciphertext (rule 72) kw_id shift, and go to state 1 '[' shift, and go to state 16 '(' shift, and go to state 17 '{' shift, and go to state 18 id go to state 19 atomic_term_or_ciphertext go to state 213 atomic_term go to state 23 state 210 assignments -> assignments ',' . assignment (rule 71) kw_id shift, and go to state 1 id go to state 195 assignment go to state 214 state 211 case -> kw_case term ':' . messages (rule 45) $default reduce using rule 34 (messages) messages go to state 215 state 212 principals -> '[' '^' ids ']' . (rule 74) $default reduce using rule 74 (principals) state 213 atomic_term_or_ciphertext -> atomic_term_or_ciphertext . '@' label id (rule 56) assignment -> id '=' atomic_term_or_ciphertext . (rule 72) '@' shift, and go to state 43 $default reduce using rule 72 (assignment) state 214 assignments -> assignments ',' assignment . (rule 71) $default reduce using rule 71 (assignments) state 215 messages -> messages . message (rule 35) case -> kw_case term ':' messages . (rule 45) kw_id shift, and go to state 1 kw_label shift, and go to state 48 kw_switch shift, and go to state 49 '{' shift, and go to state 9 $default reduce using rule 45 (case) id go to state 51 block go to state 52 message go to state 53 label go to state 54 state 216 $ go to state 217 state 217 $ go to state 218 state 218 $default accept