| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (955 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (704 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Global Index
A
acyclic [definition, in LS2NF.acyclic]acyclic [section, in LS2NF.acyclic]
acyclic [library]
acyclic_wf [lemma, in LS2NF.acyclic_wf]
acyclic_flip_wf [lemma, in LS2NF.acyclic_wf]
acyclic_wf [section, in LS2NF.acyclic_wf]
acyclic_succ_wf [lemma, in LS2NF.acyclic]
acyclic_prec_wf [lemma, in LS2NF.acyclic]
acyclic_wf [library]
acyclic0:8 [binder, in LS2NF.encoding]
Al:20 [binder, in LS2NF.grammar]
Al:66 [binder, in LS2NF.grammar]
ambiguity [section, in LS2NF.ambiguity]
ambiguity [library]
apply_binary_nil_r [lemma, in LS2NF.encoding]
apply_binary_nil_l [lemma, in LS2NF.encoding]
apply_unary_nil [lemma, in LS2NF.encoding]
app_length_le_l [lemma, in LS2NF.encoding]
app₁ [definition, in LS2NF.grammar]
app₂ [definition, in LS2NF.grammar]
Ar:21 [binder, in LS2NF.grammar]
Ar:67 [binder, in LS2NF.grammar]
atom [constructor, in LS2NF.grammar]
a':54 [binder, in LS2NF.slice]
a1:59 [binder, in LS2NF.slice]
a2:61 [binder, in LS2NF.slice]
A:1 [binder, in LS2NF.acyclic_wf]
A:1 [binder, in LS2NF.slice]
A:10 [binder, in LS2NF.ambiguity]
A:10 [binder, in LS2NF.acyclic]
a:10 [binder, in LS2NF.slice]
A:10 [binder, in LS2NF.witness]
a:10 [binder, in LS2NF.derivation]
A:10 [binder, in LS2NF.sub_derive]
A:102 [binder, in LS2NF.sub_derive]
A:105 [binder, in LS2NF.encoding]
A:106 [binder, in LS2NF.sub_derive]
A:107 [binder, in LS2NF.encoding]
A:112 [binder, in LS2NF.encoding]
A:112 [binder, in LS2NF.sub_derive]
A:12 [binder, in LS2NF.derivation]
A:124 [binder, in LS2NF.sub_derive]
A:126 [binder, in LS2NF.sub_derive]
a:13 [binder, in LS2NF.slice]
A:13 [binder, in LS2NF.sub_derive]
A:130 [binder, in LS2NF.grammar]
A:130 [binder, in LS2NF.sub_derive]
A:131 [binder, in LS2NF.grammar]
a:132 [binder, in LS2NF.grammar]
A:134 [binder, in LS2NF.grammar]
A:137 [binder, in LS2NF.grammar]
A:14 [binder, in LS2NF.ambiguity]
A:14 [binder, in LS2NF.acyclic]
A:14 [binder, in LS2NF.witness]
A:142 [binder, in LS2NF.grammar]
A:144 [binder, in LS2NF.grammar]
A:148 [binder, in LS2NF.encoding]
A:154 [binder, in LS2NF.encoding]
a:16 [binder, in LS2NF.slice]
A:16 [binder, in LS2NF.derivation]
A:173 [binder, in LS2NF.encoding]
a:18 [binder, in LS2NF.grammar]
A:180 [binder, in LS2NF.encoding]
A:187 [binder, in LS2NF.encoding]
A:19 [binder, in LS2NF.grammar]
a:19 [binder, in LS2NF.slice]
A:196 [binder, in LS2NF.encoding]
A:21 [binder, in LS2NF.sub_derive]
A:215 [binder, in LS2NF.encoding]
A:22 [binder, in LS2NF.derivation]
A:221 [binder, in LS2NF.encoding]
a:23 [binder, in LS2NF.slice]
a:23 [binder, in LS2NF.util]
A:23 [binder, in LS2NF.sub_derive]
A:24 [binder, in LS2NF.derivation]
a:26 [binder, in LS2NF.slice]
a:26 [binder, in LS2NF.derivation]
A:26 [binder, in LS2NF.sub_derive]
A:27 [binder, in LS2NF.ambiguity]
A:29 [binder, in LS2NF.sub_derive]
a:3 [binder, in LS2NF.slice]
a:30 [binder, in LS2NF.slice]
A:31 [binder, in LS2NF.encoding]
a:33 [binder, in LS2NF.slice]
A:34 [binder, in LS2NF.encoding]
A:35 [binder, in LS2NF.derivation]
A:37 [binder, in LS2NF.encoding]
a:37 [binder, in LS2NF.slice]
A:40 [binder, in LS2NF.sub_derive]
a:41 [binder, in LS2NF.slice]
A:42 [binder, in LS2NF.ambiguity]
A:44 [binder, in LS2NF.sub_derive]
a:45 [binder, in LS2NF.slice]
A:50 [binder, in LS2NF.ambiguity]
A:50 [binder, in LS2NF.sub_derive]
a:52 [binder, in LS2NF.slice]
A:55 [binder, in LS2NF.grammar]
A:56 [binder, in LS2NF.sub_derive]
a:57 [binder, in LS2NF.slice]
a:6 [binder, in LS2NF.slice]
A:6 [binder, in LS2NF.witness]
A:60 [binder, in LS2NF.sub_derive]
A:64 [binder, in LS2NF.grammar]
A:64 [binder, in LS2NF.sub_derive]
A:66 [binder, in LS2NF.encoding]
a:69 [binder, in LS2NF.encoding]
A:7 [binder, in LS2NF.acyclic]
A:7 [binder, in LS2NF.witness]
A:71 [binder, in LS2NF.ambiguity]
A:72 [binder, in LS2NF.grammar]
A:73 [binder, in LS2NF.ambiguity]
A:74 [binder, in LS2NF.sub_derive]
a:75 [binder, in LS2NF.slice]
A:78 [binder, in LS2NF.encoding]
a:79 [binder, in LS2NF.slice]
a:8 [binder, in LS2NF.witness]
A:8 [binder, in LS2NF.derivation]
A:8 [binder, in LS2NF.sub_derive]
a:81 [binder, in LS2NF.slice]
A:81 [binder, in LS2NF.sub_derive]
A:82 [binder, in LS2NF.encoding]
a:84 [binder, in LS2NF.slice]
A:85 [binder, in LS2NF.sub_derive]
A:89 [binder, in LS2NF.grammar]
A:9 [binder, in LS2NF.util]
A:9 [binder, in LS2NF.derivation]
A:91 [binder, in LS2NF.encoding]
A:91 [binder, in LS2NF.sub_derive]
A:92 [binder, in LS2NF.grammar]
A:93 [binder, in LS2NF.encoding]
A:96 [binder, in LS2NF.grammar]
A:97 [binder, in LS2NF.encoding]
B
binary [constructor, in LS2NF.grammar]binary_tree [constructor, in LS2NF.grammar]
binary_clause_predicate_unique [lemma, in LS2NF.grammar]
binary_clause_predicate [projection, in LS2NF.grammar]
binary_predicate [definition, in LS2NF.grammar]
bind_Some_is_Some [lemma, in LS2NF.ambiguity]
Bl:107 [binder, in LS2NF.sub_derive]
Bl:113 [binder, in LS2NF.sub_derive]
Bl:17 [binder, in LS2NF.derivation]
Bl:30 [binder, in LS2NF.derivation]
Bl:45 [binder, in LS2NF.sub_derive]
Bl:51 [binder, in LS2NF.sub_derive]
Bl:72 [binder, in LS2NF.encoding]
Bl:86 [binder, in LS2NF.sub_derive]
Bl:92 [binder, in LS2NF.sub_derive]
Bl:97 [binder, in LS2NF.grammar]
Br:109 [binder, in LS2NF.sub_derive]
Br:115 [binder, in LS2NF.sub_derive]
Br:18 [binder, in LS2NF.derivation]
Br:31 [binder, in LS2NF.derivation]
Br:46 [binder, in LS2NF.sub_derive]
Br:52 [binder, in LS2NF.sub_derive]
Br:73 [binder, in LS2NF.encoding]
Br:88 [binder, in LS2NF.sub_derive]
Br:94 [binder, in LS2NF.sub_derive]
Br:98 [binder, in LS2NF.grammar]
B':108 [binder, in LS2NF.encoding]
B':113 [binder, in LS2NF.encoding]
B':127 [binder, in LS2NF.sub_derive]
B':131 [binder, in LS2NF.sub_derive]
B':94 [binder, in LS2NF.encoding]
B':98 [binder, in LS2NF.encoding]
B:103 [binder, in LS2NF.sub_derive]
B:104 [binder, in LS2NF.encoding]
B:11 [binder, in LS2NF.acyclic]
B:13 [binder, in LS2NF.derivation]
B:137 [binder, in LS2NF.encoding]
B:145 [binder, in LS2NF.encoding]
B:15 [binder, in LS2NF.acyclic]
B:28 [binder, in LS2NF.ambiguity]
B:28 [binder, in LS2NF.derivation]
B:41 [binder, in LS2NF.sub_derive]
B:58 [binder, in LS2NF.sub_derive]
B:62 [binder, in LS2NF.sub_derive]
B:66 [binder, in LS2NF.sub_derive]
B:70 [binder, in LS2NF.encoding]
B:76 [binder, in LS2NF.sub_derive]
B:8 [binder, in LS2NF.acyclic]
B:82 [binder, in LS2NF.sub_derive]
B:88 [binder, in LS2NF.encoding]
B:93 [binder, in LS2NF.grammar]
C
can_reach_from [projection, in LS2NF.encoding]can_derive [projection, in LS2NF.encoding]
check_tree_eq_spec [lemma, in LS2NF.grammar]
check_tree_eq [definition, in LS2NF.grammar]
check_lf_clause_eq_spec [lemma, in LS2NF.grammar]
check_lf_clause_eq [definition, in LS2NF.grammar]
check_derive_spec [lemma, in LS2NF.derivation]
check_derive [definition, in LS2NF.derivation]
check_reachable_from_spec [lemma, in LS2NF.sub_derive]
check_reachable_from [definition, in LS2NF.sub_derive]
child [inductive, in LS2NF.sub_derive]
child_valid [lemma, in LS2NF.sub_derive]
child_right [constructor, in LS2NF.sub_derive]
child_left [constructor, in LS2NF.sub_derive]
child_unary [constructor, in LS2NF.sub_derive]
choice_clauses [definition, in LS2NF.encoding]
choice_clause [inductive, in LS2NF.encoding]
clause [inductive, in LS2NF.grammar]
clauses [section, in LS2NF.grammar]
clauses [definition, in LS2NF.grammar]
col [projection, in LS2NF.encoding]
D
decode [definition, in LS2NF.encoding]decode_encode [lemma, in LS2NF.encoding]
decode_lookup [lemma, in LS2NF.encoding]
decode_length [lemma, in LS2NF.encoding]
derivation [inductive, in LS2NF.derivation]
derivation [section, in LS2NF.derivation]
derivation [library]
derivation_spec [lemma, in LS2NF.derivation]
derive [definition, in LS2NF.grammar]
derive_amb_iff_local_amb [lemma, in LS2NF.ambiguity]
derive_amb_implies_local_amb [lemma, in LS2NF.ambiguity]
derive_amb [definition, in LS2NF.ambiguity]
derive_binary [constructor, in LS2NF.derivation]
derive_unary [constructor, in LS2NF.derivation]
derive_atom [constructor, in LS2NF.derivation]
derive_ε [constructor, in LS2NF.derivation]
diff [definition, in LS2NF.ambiguity]
diff_result_subtree [lemma, in LS2NF.ambiguity]
diff_result_not_similar [lemma, in LS2NF.ambiguity]
diff_Some_inv [lemma, in LS2NF.ambiguity]
diff_None [lemma, in LS2NF.ambiguity]
E
elem_of_clauses [lemma, in LS2NF.grammar]elem_of_choice_clauses [lemma, in LS2NF.encoding]
encode [definition, in LS2NF.encoding]
encoding [section, in LS2NF.encoding]
encoding [library]
encoding.Φ_app₂_spec [variable, in LS2NF.encoding]
encoding.Φ_app₂ [variable, in LS2NF.encoding]
encoding.Φ_app₁_spec [variable, in LS2NF.encoding]
encoding.Φ_app₁ [variable, in LS2NF.encoding]
EqDecision0:118 [binder, in LS2NF.grammar]
EqDecision0:24 [binder, in LS2NF.grammar]
EqDecision0:3 [binder, in LS2NF.encoding]
EqDecision0:3 [binder, in LS2NF.acyclic]
EqDecision0:3 [binder, in LS2NF.witness]
EqDecision0:3 [binder, in LS2NF.derivation]
EqDecision0:3 [binder, in LS2NF.sub_derive]
EqDecision0:32 [binder, in LS2NF.grammar]
EqDecision0:38 [binder, in LS2NF.grammar]
EqDecision0:6 [binder, in LS2NF.grammar]
EqDecision0:7 [binder, in LS2NF.ambiguity]
EqDecision0:8 [binder, in LS2NF.acyclic_wf]
EqDecision1:119 [binder, in LS2NF.grammar]
EqDecision1:25 [binder, in LS2NF.grammar]
EqDecision1:33 [binder, in LS2NF.grammar]
EqDecision1:39 [binder, in LS2NF.grammar]
EqDecision1:4 [binder, in LS2NF.witness]
EqDecision1:4 [binder, in LS2NF.derivation]
EqDecision1:4 [binder, in LS2NF.sub_derive]
EqDecision1:5 [binder, in LS2NF.encoding]
EqDecision1:8 [binder, in LS2NF.ambiguity]
E:12 [binder, in LS2NF.acyclic]
E:16 [binder, in LS2NF.acyclic]
F
Finite0:18 [binder, in LS2NF.acyclic]Finite0:6 [binder, in LS2NF.encoding]
Finite0:9 [binder, in LS2NF.acyclic_wf]
formula [definition, in LS2NF.encoding]
f:29 [binder, in LS2NF.ambiguity]
G
grammar [record, in LS2NF.grammar]grammar [library]
G:127 [binder, in LS2NF.grammar]
G:4 [binder, in LS2NF.acyclic]
G:5 [binder, in LS2NF.witness]
G:5 [binder, in LS2NF.derivation]
G:5 [binder, in LS2NF.sub_derive]
G:7 [binder, in LS2NF.encoding]
G:71 [binder, in LS2NF.grammar]
G:84 [binder, in LS2NF.grammar]
G:88 [binder, in LS2NF.grammar]
G:9 [binder, in LS2NF.ambiguity]
H
HdRel_Forall [lemma, in LS2NF.util]H:16 [binder, in LS2NF.ambiguity]
h:17 [binder, in LS2NF.ambiguity]
H:218 [binder, in LS2NF.encoding]
h:43 [binder, in LS2NF.slice]
H:44 [binder, in LS2NF.ambiguity]
h:45 [binder, in LS2NF.ambiguity]
I
index_range_elem_of [lemma, in LS2NF.util]index_range_lookup [lemma, in LS2NF.util]
index_range_length [lemma, in LS2NF.util]
index_range [definition, in LS2NF.util]
Inhabited0:4 [binder, in LS2NF.encoding]
i:12 [binder, in LS2NF.util]
i:13 [binder, in LS2NF.encoding]
i:18 [binder, in LS2NF.util]
i:20 [binder, in LS2NF.encoding]
i:21 [binder, in LS2NF.slice]
i:25 [binder, in LS2NF.encoding]
i:28 [binder, in LS2NF.encoding]
i:29 [binder, in LS2NF.encoding]
i:30 [binder, in LS2NF.encoding]
i:49 [binder, in LS2NF.slice]
i:58 [binder, in LS2NF.encoding]
i:6 [binder, in LS2NF.util]
J
j:13 [binder, in LS2NF.util]j:50 [binder, in LS2NF.slice]
K
k':47 [binder, in LS2NF.slice]k':55 [binder, in LS2NF.slice]
k1:34 [binder, in LS2NF.slice]
k1:38 [binder, in LS2NF.slice]
k1:60 [binder, in LS2NF.slice]
k2:35 [binder, in LS2NF.slice]
k2:39 [binder, in LS2NF.slice]
k2:62 [binder, in LS2NF.slice]
k:102 [binder, in LS2NF.encoding]
k:11 [binder, in LS2NF.slice]
k:118 [binder, in LS2NF.encoding]
k:122 [binder, in LS2NF.encoding]
k:128 [binder, in LS2NF.encoding]
k:131 [binder, in LS2NF.encoding]
k:134 [binder, in LS2NF.encoding]
k:14 [binder, in LS2NF.slice]
k:143 [binder, in LS2NF.encoding]
k:161 [binder, in LS2NF.encoding]
k:163 [binder, in LS2NF.encoding]
k:165 [binder, in LS2NF.encoding]
k:167 [binder, in LS2NF.encoding]
k:169 [binder, in LS2NF.encoding]
k:17 [binder, in LS2NF.slice]
k:183 [binder, in LS2NF.encoding]
k:19 [binder, in LS2NF.encoding]
k:192 [binder, in LS2NF.encoding]
k:20 [binder, in LS2NF.slice]
k:216 [binder, in LS2NF.encoding]
k:22 [binder, in LS2NF.encoding]
k:22 [binder, in LS2NF.util]
k:222 [binder, in LS2NF.encoding]
k:225 [binder, in LS2NF.encoding]
k:24 [binder, in LS2NF.encoding]
k:27 [binder, in LS2NF.slice]
k:31 [binder, in LS2NF.slice]
k:4 [binder, in LS2NF.slice]
k:42 [binder, in LS2NF.slice]
k:44 [binder, in LS2NF.encoding]
k:46 [binder, in LS2NF.slice]
k:53 [binder, in LS2NF.encoding]
k:53 [binder, in LS2NF.slice]
k:56 [binder, in LS2NF.encoding]
k:58 [binder, in LS2NF.slice]
k:61 [binder, in LS2NF.encoding]
k:64 [binder, in LS2NF.encoding]
k:8 [binder, in LS2NF.slice]
k:80 [binder, in LS2NF.encoding]
k:82 [binder, in LS2NF.slice]
k:85 [binder, in LS2NF.slice]
k:86 [binder, in LS2NF.encoding]
L
lf_clauses_no_dup [projection, in LS2NF.grammar]lf_clauses [projection, in LS2NF.grammar]
lf_clause_eq_dec [instance, in LS2NF.grammar]
lf_binary [constructor, in LS2NF.grammar]
lf_unary [constructor, in LS2NF.grammar]
lf_atom [constructor, in LS2NF.grammar]
lf_ε [constructor, in LS2NF.grammar]
lf_clause [inductive, in LS2NF.grammar]
lhs:79 [binder, in LS2NF.grammar]
line [projection, in LS2NF.encoding]
line_col [projection, in LS2NF.encoding]
list_nonempty_length [lemma, in LS2NF.encoding]
local_amb_implies_derive_amb [lemma, in LS2NF.ambiguity]
local_amb [definition, in LS2NF.ambiguity]
l':63 [binder, in LS2NF.slice]
l':73 [binder, in LS2NF.slice]
l1:188 [binder, in LS2NF.encoding]
l1:65 [binder, in LS2NF.slice]
l1:68 [binder, in LS2NF.slice]
l1:71 [binder, in LS2NF.slice]
l1:77 [binder, in LS2NF.slice]
l1:86 [binder, in LS2NF.slice]
l2:189 [binder, in LS2NF.encoding]
l2:66 [binder, in LS2NF.slice]
l2:69 [binder, in LS2NF.slice]
l2:72 [binder, in LS2NF.slice]
l2:78 [binder, in LS2NF.slice]
l2:87 [binder, in LS2NF.slice]
l:11 [binder, in LS2NF.util]
l:12 [binder, in LS2NF.slice]
l:15 [binder, in LS2NF.slice]
l:17 [binder, in LS2NF.util]
l:18 [binder, in LS2NF.slice]
l:190 [binder, in LS2NF.encoding]
l:2 [binder, in LS2NF.slice]
l:21 [binder, in LS2NF.util]
l:22 [binder, in LS2NF.slice]
l:24 [binder, in LS2NF.util]
l:25 [binder, in LS2NF.slice]
l:26 [binder, in LS2NF.util]
l:27 [binder, in LS2NF.util]
l:29 [binder, in LS2NF.slice]
l:32 [binder, in LS2NF.slice]
l:36 [binder, in LS2NF.slice]
l:40 [binder, in LS2NF.slice]
l:44 [binder, in LS2NF.slice]
l:48 [binder, in LS2NF.slice]
l:5 [binder, in LS2NF.slice]
l:51 [binder, in LS2NF.slice]
l:56 [binder, in LS2NF.slice]
l:64 [binder, in LS2NF.slice]
l:67 [binder, in LS2NF.slice]
l:7 [binder, in LS2NF.slice]
l:70 [binder, in LS2NF.slice]
l:74 [binder, in LS2NF.slice]
l:76 [binder, in LS2NF.slice]
l:79 [binder, in LS2NF.encoding]
l:80 [binder, in LS2NF.slice]
l:83 [binder, in LS2NF.slice]
l:9 [binder, in LS2NF.slice]
M
mk_production [constructor, in LS2NF.grammar]model [record, in LS2NF.encoding]
monotone [definition, in LS2NF.util]
monotone_trans_alt_spec [lemma, in LS2NF.util]
monotone_trans_alt [definition, in LS2NF.util]
mx:30 [binder, in LS2NF.ambiguity]
m:103 [binder, in LS2NF.encoding]
m:119 [binder, in LS2NF.encoding]
m:136 [binder, in LS2NF.encoding]
m:144 [binder, in LS2NF.encoding]
m:162 [binder, in LS2NF.encoding]
m:164 [binder, in LS2NF.encoding]
m:166 [binder, in LS2NF.encoding]
m:168 [binder, in LS2NF.encoding]
m:170 [binder, in LS2NF.encoding]
m:18 [binder, in LS2NF.encoding]
m:184 [binder, in LS2NF.encoding]
m:193 [binder, in LS2NF.encoding]
m:21 [binder, in LS2NF.encoding]
m:217 [binder, in LS2NF.encoding]
m:223 [binder, in LS2NF.encoding]
m:227 [binder, in LS2NF.encoding]
m:23 [binder, in LS2NF.encoding]
m:45 [binder, in LS2NF.encoding]
m:54 [binder, in LS2NF.encoding]
m:57 [binder, in LS2NF.encoding]
m:62 [binder, in LS2NF.encoding]
m:65 [binder, in LS2NF.encoding]
m:81 [binder, in LS2NF.encoding]
m:87 [binder, in LS2NF.encoding]
N
NoDup_lookup_in_range [lemma, in LS2NF.slice]n:1 [binder, in LS2NF.util]
N:102 [binder, in LS2NF.grammar]
N:15 [binder, in LS2NF.grammar]
N:2 [binder, in LS2NF.ambiguity]
N:2 [binder, in LS2NF.encoding]
N:2 [binder, in LS2NF.acyclic]
N:2 [binder, in LS2NF.witness]
N:2 [binder, in LS2NF.derivation]
N:2 [binder, in LS2NF.sub_derive]
N:23 [binder, in LS2NF.grammar]
N:31 [binder, in LS2NF.grammar]
N:37 [binder, in LS2NF.grammar]
n:4 [binder, in LS2NF.util]
n:5 [binder, in LS2NF.util]
N:51 [binder, in LS2NF.grammar]
N:60 [binder, in LS2NF.grammar]
n:7 [binder, in LS2NF.util]
N:70 [binder, in LS2NF.grammar]
N:76 [binder, in LS2NF.grammar]
N:82 [binder, in LS2NF.grammar]
N:87 [binder, in LS2NF.grammar]
P
parsing [section, in LS2NF.grammar]pos [projection, in LS2NF.grammar]
pos_token_lt_trans [instance, in LS2NF.grammar]
pos_token_lt [definition, in LS2NF.grammar]
pos_token_eq_dec [instance, in LS2NF.grammar]
pos_token [record, in LS2NF.grammar]
prec [definition, in LS2NF.acyclic]
production [inductive, in LS2NF.grammar]
production_elem_of_grammar [instance, in LS2NF.grammar]
pt1:8 [binder, in LS2NF.grammar]
pt2:9 [binder, in LS2NF.grammar]
pt:107 [binder, in LS2NF.grammar]
p:11 [binder, in LS2NF.derivation]
p:133 [binder, in LS2NF.grammar]
p:176 [binder, in LS2NF.encoding]
P:191 [binder, in LS2NF.encoding]
p:27 [binder, in LS2NF.derivation]
p:41 [binder, in LS2NF.grammar]
p:45 [binder, in LS2NF.grammar]
p:83 [binder, in LS2NF.grammar]
p:9 [binder, in LS2NF.witness]
R
reachable [definition, in LS2NF.sub_derive]reachable_from_spec [lemma, in LS2NF.sub_derive]
reachable_from_right [constructor, in LS2NF.sub_derive]
reachable_from_left [constructor, in LS2NF.sub_derive]
reachable_from_unary [constructor, in LS2NF.sub_derive]
reachable_from_refl [constructor, in LS2NF.sub_derive]
reachable_from [inductive, in LS2NF.sub_derive]
reachable_to_spec [lemma, in LS2NF.sub_derive]
reachable_to_right [constructor, in LS2NF.sub_derive]
reachable_to_left [constructor, in LS2NF.sub_derive]
reachable_to_unary [constructor, in LS2NF.sub_derive]
reachable_to_refl [constructor, in LS2NF.sub_derive]
reachable_to [inductive, in LS2NF.sub_derive]
reachable_sublist [lemma, in LS2NF.sub_derive]
reachable_sub_sig [lemma, in LS2NF.sub_derive]
reachable_spec [lemma, in LS2NF.sub_derive]
rel_acyclic [definition, in LS2NF.acyclic_wf]
replace [definition, in LS2NF.ambiguity]
replace_subtree [lemma, in LS2NF.ambiguity]
replace_witness [lemma, in LS2NF.ambiguity]
replace_id [lemma, in LS2NF.ambiguity]
replace_Some [lemma, in LS2NF.ambiguity]
rhs:80 [binder, in LS2NF.grammar]
root [definition, in LS2NF.grammar]
R:10 [binder, in LS2NF.util]
r:105 [binder, in LS2NF.grammar]
r:106 [binder, in LS2NF.grammar]
r:108 [binder, in LS2NF.grammar]
r:110 [binder, in LS2NF.grammar]
R:2 [binder, in LS2NF.acyclic_wf]
R:6 [binder, in LS2NF.acyclic_wf]
S
sentence [definition, in LS2NF.grammar]sig [definition, in LS2NF.sub_derive]
similar [definition, in LS2NF.ambiguity]
similar_refl [lemma, in LS2NF.ambiguity]
slice [definition, in LS2NF.slice]
slice [section, in LS2NF.slice]
slice [library]
slice_app_inv_NoDup [lemma, in LS2NF.slice]
slice_sublist [lemma, in LS2NF.slice]
slice_app_inv_NoDup_aux [lemma, in LS2NF.slice]
slice_eq_inv_NoDup [lemma, in LS2NF.slice]
slice_eq_inv [lemma, in LS2NF.slice]
slice_split [lemma, in LS2NF.slice]
slice_app_2 [lemma, in LS2NF.slice]
slice_app_1 [lemma, in LS2NF.slice]
slice_full_iff [lemma, in LS2NF.slice]
slice_singleton_iff [lemma, in LS2NF.slice]
slice_singleton [lemma, in LS2NF.slice]
slice_lookup [lemma, in LS2NF.slice]
slice_nonempty_iff [lemma, in LS2NF.slice]
slice_nil_iff [lemma, in LS2NF.slice]
slice_length [lemma, in LS2NF.slice]
slice_full [lemma, in LS2NF.slice]
slice_nil [lemma, in LS2NF.slice]
Sorted_monotone [lemma, in LS2NF.util]
Sorted_cons_iff [lemma, in LS2NF.util]
Sorted_lemmas [section, in LS2NF.util]
start [projection, in LS2NF.grammar]
step [inductive, in LS2NF.sub_derive]
step_sub [lemma, in LS2NF.sub_derive]
step_spec [lemma, in LS2NF.sub_derive]
step_right [constructor, in LS2NF.sub_derive]
step_left [constructor, in LS2NF.sub_derive]
step_unary [constructor, in LS2NF.sub_derive]
sublist [definition, in LS2NF.slice]
sublist_app_slice_NoDup [lemma, in LS2NF.slice]
sublist_slice [lemma, in LS2NF.slice]
sublist_app_r [lemma, in LS2NF.slice]
sublist_app_l [lemma, in LS2NF.slice]
subtree [definition, in LS2NF.sub_derive]
subtree_binary_inv [lemma, in LS2NF.sub_derive]
subtree_unary_inv [lemma, in LS2NF.sub_derive]
subtree_token_inv [lemma, in LS2NF.sub_derive]
subtree_ε_inv [lemma, in LS2NF.sub_derive]
subtree_valid [lemma, in LS2NF.sub_derive]
_ →∗ _ [notation, in LS2NF.sub_derive]
_ →₁ _ [notation, in LS2NF.sub_derive]
sub_derive_trans [instance, in LS2NF.sub_derive]
sub_derive [definition, in LS2NF.sub_derive]
sub_derive [section, in LS2NF.sub_derive]
sub_derive [library]
succ [inductive, in LS2NF.acyclic]
succ_right [constructor, in LS2NF.acyclic]
succ_left [constructor, in LS2NF.acyclic]
succ_unary [constructor, in LS2NF.acyclic]
S:101 [binder, in LS2NF.encoding]
S:117 [binder, in LS2NF.encoding]
S:135 [binder, in LS2NF.encoding]
S:142 [binder, in LS2NF.encoding]
s:22 [binder, in LS2NF.ambiguity]
S:26 [binder, in LS2NF.encoding]
s:34 [binder, in LS2NF.ambiguity]
s:37 [binder, in LS2NF.ambiguity]
S:38 [binder, in LS2NF.encoding]
s:40 [binder, in LS2NF.ambiguity]
s:48 [binder, in LS2NF.ambiguity]
S:85 [binder, in LS2NF.encoding]
T
tc_flip [lemma, in LS2NF.acyclic_wf]tc_refl_ex_loop [lemma, in LS2NF.acyclic_wf]
term [projection, in LS2NF.encoding]
tk:24 [binder, in LS2NF.sub_derive]
tl:111 [binder, in LS2NF.grammar]
tl:30 [binder, in LS2NF.sub_derive]
token [projection, in LS2NF.grammar]
token_tree [constructor, in LS2NF.grammar]
token:63 [binder, in LS2NF.grammar]
Transitive0:16 [binder, in LS2NF.util]
tree [inductive, in LS2NF.grammar]
tree_witness [definition, in LS2NF.grammar]
tree_valid [inductive, in LS2NF.grammar]
tree_eq_dec [instance, in LS2NF.grammar]
tr':26 [binder, in LS2NF.ambiguity]
tr:112 [binder, in LS2NF.grammar]
tr:31 [binder, in LS2NF.sub_derive]
t':12 [binder, in LS2NF.sub_derive]
t':135 [binder, in LS2NF.grammar]
t':15 [binder, in LS2NF.sub_derive]
t':17 [binder, in LS2NF.sub_derive]
t':19 [binder, in LS2NF.sub_derive]
t':25 [binder, in LS2NF.sub_derive]
t':28 [binder, in LS2NF.sub_derive]
t':36 [binder, in LS2NF.sub_derive]
T':41 [binder, in LS2NF.ambiguity]
T':49 [binder, in LS2NF.ambiguity]
t1':25 [binder, in LS2NF.ambiguity]
t1':61 [binder, in LS2NF.ambiguity]
t1':65 [binder, in LS2NF.ambiguity]
t1':69 [binder, in LS2NF.ambiguity]
t1:12 [binder, in LS2NF.ambiguity]
t1:120 [binder, in LS2NF.grammar]
t1:125 [binder, in LS2NF.grammar]
t1:138 [binder, in LS2NF.grammar]
t1:16 [binder, in LS2NF.witness]
t1:178 [binder, in LS2NF.encoding]
t1:18 [binder, in LS2NF.ambiguity]
t1:197 [binder, in LS2NF.encoding]
t1:211 [binder, in LS2NF.encoding]
t1:213 [binder, in LS2NF.encoding]
t1:3 [binder, in LS2NF.ambiguity]
t1:52 [binder, in LS2NF.ambiguity]
t1:57 [binder, in LS2NF.ambiguity]
t1:59 [binder, in LS2NF.ambiguity]
t1:63 [binder, in LS2NF.ambiguity]
t1:67 [binder, in LS2NF.ambiguity]
t2':62 [binder, in LS2NF.ambiguity]
t2':66 [binder, in LS2NF.ambiguity]
t2':70 [binder, in LS2NF.ambiguity]
t2:121 [binder, in LS2NF.grammar]
t2:126 [binder, in LS2NF.grammar]
t2:13 [binder, in LS2NF.ambiguity]
t2:139 [binder, in LS2NF.grammar]
t2:17 [binder, in LS2NF.witness]
t2:179 [binder, in LS2NF.encoding]
t2:19 [binder, in LS2NF.ambiguity]
t2:198 [binder, in LS2NF.encoding]
t2:212 [binder, in LS2NF.encoding]
t2:214 [binder, in LS2NF.encoding]
t2:4 [binder, in LS2NF.ambiguity]
t2:53 [binder, in LS2NF.ambiguity]
t2:58 [binder, in LS2NF.ambiguity]
t2:60 [binder, in LS2NF.ambiguity]
t2:64 [binder, in LS2NF.ambiguity]
t2:68 [binder, in LS2NF.ambiguity]
t:109 [binder, in LS2NF.grammar]
t:11 [binder, in LS2NF.sub_derive]
t:113 [binder, in LS2NF.grammar]
t:115 [binder, in LS2NF.grammar]
t:12 [binder, in LS2NF.witness]
t:14 [binder, in LS2NF.sub_derive]
t:141 [binder, in LS2NF.grammar]
t:146 [binder, in LS2NF.grammar]
t:16 [binder, in LS2NF.sub_derive]
t:177 [binder, in LS2NF.encoding]
t:18 [binder, in LS2NF.sub_derive]
t:199 [binder, in LS2NF.encoding]
T:20 [binder, in LS2NF.ambiguity]
t:20 [binder, in LS2NF.sub_derive]
t:200 [binder, in LS2NF.encoding]
t:209 [binder, in LS2NF.encoding]
t:21 [binder, in LS2NF.ambiguity]
t:210 [binder, in LS2NF.encoding]
t:22 [binder, in LS2NF.sub_derive]
t:27 [binder, in LS2NF.sub_derive]
T:32 [binder, in LS2NF.ambiguity]
t:33 [binder, in LS2NF.ambiguity]
T:35 [binder, in LS2NF.ambiguity]
t:36 [binder, in LS2NF.ambiguity]
t:37 [binder, in LS2NF.sub_derive]
T:38 [binder, in LS2NF.ambiguity]
t:39 [binder, in LS2NF.ambiguity]
T:46 [binder, in LS2NF.ambiguity]
t:47 [binder, in LS2NF.ambiguity]
t:9 [binder, in LS2NF.sub_derive]
U
unary [constructor, in LS2NF.grammar]unary_tree [constructor, in LS2NF.grammar]
unary_clause_predicate_unique [lemma, in LS2NF.grammar]
unary_clause_predicate [projection, in LS2NF.grammar]
unary_predicate [definition, in LS2NF.grammar]
using_binary [constructor, in LS2NF.encoding]
using_unary [constructor, in LS2NF.encoding]
using_atom [constructor, in LS2NF.encoding]
using_ε [constructor, in LS2NF.encoding]
util [library]
V
valid_binary [constructor, in LS2NF.grammar]valid_unary [constructor, in LS2NF.grammar]
valid_token [constructor, in LS2NF.grammar]
valid_ε [constructor, in LS2NF.grammar]
vl:68 [binder, in LS2NF.sub_derive]
vl:72 [binder, in LS2NF.sub_derive]
vr:69 [binder, in LS2NF.sub_derive]
vr:73 [binder, in LS2NF.sub_derive]
v:59 [binder, in LS2NF.sub_derive]
v:63 [binder, in LS2NF.sub_derive]
v:67 [binder, in LS2NF.sub_derive]
v:77 [binder, in LS2NF.sub_derive]
W
well_formed [definition, in LS2NF.grammar]well_formed_no_dup [lemma, in LS2NF.encoding]
witness [section, in LS2NF.witness]
witness [library]
witness_binary [lemma, in LS2NF.witness]
witness_unary [lemma, in LS2NF.witness]
witness_atom [lemma, in LS2NF.witness]
witness_ε [lemma, in LS2NF.witness]
wl:48 [binder, in LS2NF.sub_derive]
wl:54 [binder, in LS2NF.sub_derive]
word [definition, in LS2NF.grammar]
wrap_with_id [lemma, in LS2NF.encoding]
wr:49 [binder, in LS2NF.sub_derive]
wr:55 [binder, in LS2NF.sub_derive]
w':129 [binder, in LS2NF.sub_derive]
w':133 [binder, in LS2NF.sub_derive]
w1:108 [binder, in LS2NF.sub_derive]
w1:114 [binder, in LS2NF.sub_derive]
w1:20 [binder, in LS2NF.derivation]
w1:33 [binder, in LS2NF.derivation]
w1:46 [binder, in LS2NF.grammar]
w1:87 [binder, in LS2NF.sub_derive]
w1:93 [binder, in LS2NF.sub_derive]
w2:110 [binder, in LS2NF.sub_derive]
w2:116 [binder, in LS2NF.sub_derive]
w2:18 [binder, in LS2NF.witness]
w2:21 [binder, in LS2NF.derivation]
w2:34 [binder, in LS2NF.derivation]
w2:47 [binder, in LS2NF.grammar]
w2:89 [binder, in LS2NF.sub_derive]
w2:95 [binder, in LS2NF.sub_derive]
w:104 [binder, in LS2NF.sub_derive]
w:11 [binder, in LS2NF.ambiguity]
w:121 [binder, in LS2NF.encoding]
w:125 [binder, in LS2NF.encoding]
w:127 [binder, in LS2NF.encoding]
w:13 [binder, in LS2NF.grammar]
w:13 [binder, in LS2NF.witness]
w:130 [binder, in LS2NF.encoding]
w:133 [binder, in LS2NF.encoding]
w:143 [binder, in LS2NF.grammar]
w:145 [binder, in LS2NF.grammar]
w:15 [binder, in LS2NF.ambiguity]
w:15 [binder, in LS2NF.derivation]
w:226 [binder, in LS2NF.encoding]
w:23 [binder, in LS2NF.derivation]
w:25 [binder, in LS2NF.derivation]
w:27 [binder, in LS2NF.encoding]
w:36 [binder, in LS2NF.derivation]
w:39 [binder, in LS2NF.encoding]
w:43 [binder, in LS2NF.ambiguity]
w:43 [binder, in LS2NF.sub_derive]
w:51 [binder, in LS2NF.ambiguity]
w:57 [binder, in LS2NF.sub_derive]
w:60 [binder, in LS2NF.encoding]
w:61 [binder, in LS2NF.sub_derive]
w:63 [binder, in LS2NF.encoding]
w:65 [binder, in LS2NF.sub_derive]
w:72 [binder, in LS2NF.ambiguity]
w:74 [binder, in LS2NF.ambiguity]
w:75 [binder, in LS2NF.sub_derive]
w:77 [binder, in LS2NF.encoding]
w:83 [binder, in LS2NF.sub_derive]
X
x1:49 [binder, in LS2NF.encoding]x2:51 [binder, in LS2NF.encoding]
x:110 [binder, in LS2NF.encoding]
x:115 [binder, in LS2NF.encoding]
X:120 [binder, in LS2NF.encoding]
X:129 [binder, in LS2NF.encoding]
X:132 [binder, in LS2NF.encoding]
x:138 [binder, in LS2NF.encoding]
x:14 [binder, in LS2NF.util]
x:158 [binder, in LS2NF.encoding]
x:171 [binder, in LS2NF.encoding]
x:181 [binder, in LS2NF.encoding]
x:19 [binder, in LS2NF.util]
x:194 [binder, in LS2NF.encoding]
x:219 [binder, in LS2NF.encoding]
X:224 [binder, in LS2NF.encoding]
x:24 [binder, in LS2NF.slice]
x:25 [binder, in LS2NF.util]
x:28 [binder, in LS2NF.slice]
x:3 [binder, in LS2NF.acyclic_wf]
x:31 [binder, in LS2NF.ambiguity]
x:32 [binder, in LS2NF.encoding]
x:35 [binder, in LS2NF.encoding]
x:4 [binder, in LS2NF.acyclic_wf]
x:42 [binder, in LS2NF.encoding]
X:59 [binder, in LS2NF.encoding]
x:67 [binder, in LS2NF.encoding]
x:7 [binder, in LS2NF.acyclic_wf]
X:76 [binder, in LS2NF.encoding]
x:8 [binder, in LS2NF.util]
x:83 [binder, in LS2NF.encoding]
x:89 [binder, in LS2NF.encoding]
Y
y:15 [binder, in LS2NF.util]y:20 [binder, in LS2NF.util]
y:5 [binder, in LS2NF.acyclic_wf]
other
_ ⊨ _ => _ (grammar_scope) [notation, in LS2NF.grammar]_ ▷ _ ={ _ }=> _ (grammar_scope) [notation, in LS2NF.grammar]
✓{ _ } _ (grammar_scope) [notation, in LS2NF.grammar]
_ ↦ _ (grammar_scope) [notation, in LS2NF.grammar]
_ @ _ (grammar_scope) [notation, in LS2NF.grammar]
Σ:1 [binder, in LS2NF.grammar]
Σ:1 [binder, in LS2NF.ambiguity]
Σ:1 [binder, in LS2NF.encoding]
Σ:1 [binder, in LS2NF.acyclic]
Σ:1 [binder, in LS2NF.witness]
Σ:1 [binder, in LS2NF.derivation]
Σ:1 [binder, in LS2NF.sub_derive]
Σ:10 [binder, in LS2NF.grammar]
Σ:101 [binder, in LS2NF.grammar]
Σ:11 [binder, in LS2NF.grammar]
Σ:12 [binder, in LS2NF.grammar]
Σ:14 [binder, in LS2NF.grammar]
Σ:22 [binder, in LS2NF.grammar]
Σ:30 [binder, in LS2NF.grammar]
Σ:36 [binder, in LS2NF.grammar]
Σ:40 [binder, in LS2NF.grammar]
Σ:42 [binder, in LS2NF.grammar]
Σ:44 [binder, in LS2NF.grammar]
Σ:48 [binder, in LS2NF.grammar]
Σ:5 [binder, in LS2NF.grammar]
Σ:50 [binder, in LS2NF.grammar]
Σ:59 [binder, in LS2NF.grammar]
Σ:69 [binder, in LS2NF.grammar]
Σ:7 [binder, in LS2NF.grammar]
Σ:75 [binder, in LS2NF.grammar]
Σ:81 [binder, in LS2NF.grammar]
Σ:86 [binder, in LS2NF.grammar]
Φ_amb_complete [lemma, in LS2NF.encoding]
Φ_amb_sound [lemma, in LS2NF.encoding]
Φ_amb [definition, in LS2NF.encoding]
Φ_multi_spec [lemma, in LS2NF.encoding]
Φ_multi [definition, in LS2NF.encoding]
Φ_choice_sem_witness [lemma, in LS2NF.encoding]
Φ_choice_sem [definition, in LS2NF.encoding]
Φ_reach_empty_spec [lemma, in LS2NF.encoding]
Φ_reach_nonempty_spec [lemma, in LS2NF.encoding]
Φ_reach_sat [lemma, in LS2NF.encoding]
Φ_reach_empty_sat [lemma, in LS2NF.encoding]
Φ_reach_nonempty_sat [lemma, in LS2NF.encoding]
Φ_reach [definition, in LS2NF.encoding]
Φ_reach_empty [definition, in LS2NF.encoding]
Φ_reach_nonempty [definition, in LS2NF.encoding]
Φ_derive_spec [lemma, in LS2NF.encoding]
Φ_derive_sat [lemma, in LS2NF.encoding]
Φ_derive [definition, in LS2NF.encoding]
Φ_well_formed_spec [lemma, in LS2NF.encoding]
Φ_well_formed_sat [lemma, in LS2NF.encoding]
Φ_well_formed [definition, in LS2NF.encoding]
α:150 [binder, in LS2NF.encoding]
α:26 [binder, in LS2NF.grammar]
α:34 [binder, in LS2NF.grammar]
α:73 [binder, in LS2NF.grammar]
α:90 [binder, in LS2NF.grammar]
β:27 [binder, in LS2NF.grammar]
β:35 [binder, in LS2NF.grammar]
δ':100 [binder, in LS2NF.encoding]
δ':152 [binder, in LS2NF.encoding]
δ':75 [binder, in LS2NF.encoding]
δ':96 [binder, in LS2NF.encoding]
δ1:50 [binder, in LS2NF.encoding]
δ2:52 [binder, in LS2NF.encoding]
δ:111 [binder, in LS2NF.encoding]
δ:116 [binder, in LS2NF.encoding]
δ:139 [binder, in LS2NF.encoding]
δ:140 [binder, in LS2NF.encoding]
δ:141 [binder, in LS2NF.encoding]
δ:149 [binder, in LS2NF.encoding]
δ:155 [binder, in LS2NF.encoding]
δ:159 [binder, in LS2NF.encoding]
δ:172 [binder, in LS2NF.encoding]
δ:182 [binder, in LS2NF.encoding]
δ:195 [binder, in LS2NF.encoding]
δ:220 [binder, in LS2NF.encoding]
δ:33 [binder, in LS2NF.encoding]
δ:36 [binder, in LS2NF.encoding]
δ:43 [binder, in LS2NF.encoding]
δ:68 [binder, in LS2NF.encoding]
δ:84 [binder, in LS2NF.encoding]
δ:90 [binder, in LS2NF.encoding]
ε [constructor, in LS2NF.grammar]
ε_tree [constructor, in LS2NF.grammar]
ε_can_reach_from [projection, in LS2NF.encoding]
σ1:32 [binder, in LS2NF.sub_derive]
σ2:33 [binder, in LS2NF.sub_derive]
σ:118 [binder, in LS2NF.sub_derive]
σ:120 [binder, in LS2NF.sub_derive]
σ:134 [binder, in LS2NF.sub_derive]
σ:70 [binder, in LS2NF.sub_derive]
σ:78 [binder, in LS2NF.sub_derive]
σ:97 [binder, in LS2NF.sub_derive]
σ:99 [binder, in LS2NF.sub_derive]
τ:119 [binder, in LS2NF.sub_derive]
τ:121 [binder, in LS2NF.sub_derive]
τ:135 [binder, in LS2NF.sub_derive]
τ:71 [binder, in LS2NF.sub_derive]
τ:98 [binder, in LS2NF.sub_derive]
φ':100 [binder, in LS2NF.grammar]
φ':95 [binder, in LS2NF.grammar]
φ:105 [binder, in LS2NF.sub_derive]
φ:106 [binder, in LS2NF.encoding]
φ:109 [binder, in LS2NF.encoding]
φ:11 [binder, in LS2NF.witness]
φ:111 [binder, in LS2NF.sub_derive]
φ:114 [binder, in LS2NF.encoding]
φ:117 [binder, in LS2NF.sub_derive]
φ:123 [binder, in LS2NF.encoding]
φ:124 [binder, in LS2NF.encoding]
φ:125 [binder, in LS2NF.sub_derive]
φ:126 [binder, in LS2NF.encoding]
φ:128 [binder, in LS2NF.sub_derive]
φ:13 [binder, in LS2NF.acyclic]
φ:132 [binder, in LS2NF.sub_derive]
φ:136 [binder, in LS2NF.grammar]
φ:14 [binder, in LS2NF.derivation]
φ:140 [binder, in LS2NF.grammar]
φ:15 [binder, in LS2NF.witness]
φ:17 [binder, in LS2NF.acyclic]
φ:19 [binder, in LS2NF.derivation]
φ:29 [binder, in LS2NF.derivation]
φ:32 [binder, in LS2NF.derivation]
φ:41 [binder, in LS2NF.encoding]
φ:42 [binder, in LS2NF.sub_derive]
φ:43 [binder, in LS2NF.grammar]
φ:47 [binder, in LS2NF.sub_derive]
φ:48 [binder, in LS2NF.encoding]
φ:49 [binder, in LS2NF.grammar]
φ:53 [binder, in LS2NF.sub_derive]
φ:65 [binder, in LS2NF.grammar]
φ:68 [binder, in LS2NF.grammar]
φ:71 [binder, in LS2NF.encoding]
φ:74 [binder, in LS2NF.encoding]
φ:84 [binder, in LS2NF.sub_derive]
φ:9 [binder, in LS2NF.acyclic]
φ:90 [binder, in LS2NF.sub_derive]
φ:92 [binder, in LS2NF.encoding]
φ:94 [binder, in LS2NF.grammar]
φ:95 [binder, in LS2NF.encoding]
φ:96 [binder, in LS2NF.sub_derive]
φ:99 [binder, in LS2NF.grammar]
φ:99 [binder, in LS2NF.encoding]
ψ1:185 [binder, in LS2NF.encoding]
ψ2:186 [binder, in LS2NF.encoding]
ψ:153 [binder, in LS2NF.encoding]
ψ:157 [binder, in LS2NF.encoding]
ψ:174 [binder, in LS2NF.encoding]
ψ:201 [binder, in LS2NF.encoding]
ψ:202 [binder, in LS2NF.encoding]
ψ:203 [binder, in LS2NF.encoding]
ψ:204 [binder, in LS2NF.encoding]
ψ:205 [binder, in LS2NF.encoding]
ψ:206 [binder, in LS2NF.encoding]
ψ:207 [binder, in LS2NF.encoding]
ψ:208 [binder, in LS2NF.encoding]
Notation Index
S
_ →∗ _ [in LS2NF.sub_derive]_ →₁ _ [in LS2NF.sub_derive]
other
_ ⊨ _ => _ (grammar_scope) [in LS2NF.grammar]_ ▷ _ ={ _ }=> _ (grammar_scope) [in LS2NF.grammar]
✓{ _ } _ (grammar_scope) [in LS2NF.grammar]
_ ↦ _ (grammar_scope) [in LS2NF.grammar]
_ @ _ (grammar_scope) [in LS2NF.grammar]
Binder Index
A
acyclic0:8 [in LS2NF.encoding]Al:20 [in LS2NF.grammar]
Al:66 [in LS2NF.grammar]
Ar:21 [in LS2NF.grammar]
Ar:67 [in LS2NF.grammar]
a':54 [in LS2NF.slice]
a1:59 [in LS2NF.slice]
a2:61 [in LS2NF.slice]
A:1 [in LS2NF.acyclic_wf]
A:1 [in LS2NF.slice]
A:10 [in LS2NF.ambiguity]
A:10 [in LS2NF.acyclic]
a:10 [in LS2NF.slice]
A:10 [in LS2NF.witness]
a:10 [in LS2NF.derivation]
A:10 [in LS2NF.sub_derive]
A:102 [in LS2NF.sub_derive]
A:105 [in LS2NF.encoding]
A:106 [in LS2NF.sub_derive]
A:107 [in LS2NF.encoding]
A:112 [in LS2NF.encoding]
A:112 [in LS2NF.sub_derive]
A:12 [in LS2NF.derivation]
A:124 [in LS2NF.sub_derive]
A:126 [in LS2NF.sub_derive]
a:13 [in LS2NF.slice]
A:13 [in LS2NF.sub_derive]
A:130 [in LS2NF.grammar]
A:130 [in LS2NF.sub_derive]
A:131 [in LS2NF.grammar]
a:132 [in LS2NF.grammar]
A:134 [in LS2NF.grammar]
A:137 [in LS2NF.grammar]
A:14 [in LS2NF.ambiguity]
A:14 [in LS2NF.acyclic]
A:14 [in LS2NF.witness]
A:142 [in LS2NF.grammar]
A:144 [in LS2NF.grammar]
A:148 [in LS2NF.encoding]
A:154 [in LS2NF.encoding]
a:16 [in LS2NF.slice]
A:16 [in LS2NF.derivation]
A:173 [in LS2NF.encoding]
a:18 [in LS2NF.grammar]
A:180 [in LS2NF.encoding]
A:187 [in LS2NF.encoding]
A:19 [in LS2NF.grammar]
a:19 [in LS2NF.slice]
A:196 [in LS2NF.encoding]
A:21 [in LS2NF.sub_derive]
A:215 [in LS2NF.encoding]
A:22 [in LS2NF.derivation]
A:221 [in LS2NF.encoding]
a:23 [in LS2NF.slice]
a:23 [in LS2NF.util]
A:23 [in LS2NF.sub_derive]
A:24 [in LS2NF.derivation]
a:26 [in LS2NF.slice]
a:26 [in LS2NF.derivation]
A:26 [in LS2NF.sub_derive]
A:27 [in LS2NF.ambiguity]
A:29 [in LS2NF.sub_derive]
a:3 [in LS2NF.slice]
a:30 [in LS2NF.slice]
A:31 [in LS2NF.encoding]
a:33 [in LS2NF.slice]
A:34 [in LS2NF.encoding]
A:35 [in LS2NF.derivation]
A:37 [in LS2NF.encoding]
a:37 [in LS2NF.slice]
A:40 [in LS2NF.sub_derive]
a:41 [in LS2NF.slice]
A:42 [in LS2NF.ambiguity]
A:44 [in LS2NF.sub_derive]
a:45 [in LS2NF.slice]
A:50 [in LS2NF.ambiguity]
A:50 [in LS2NF.sub_derive]
a:52 [in LS2NF.slice]
A:55 [in LS2NF.grammar]
A:56 [in LS2NF.sub_derive]
a:57 [in LS2NF.slice]
a:6 [in LS2NF.slice]
A:6 [in LS2NF.witness]
A:60 [in LS2NF.sub_derive]
A:64 [in LS2NF.grammar]
A:64 [in LS2NF.sub_derive]
A:66 [in LS2NF.encoding]
a:69 [in LS2NF.encoding]
A:7 [in LS2NF.acyclic]
A:7 [in LS2NF.witness]
A:71 [in LS2NF.ambiguity]
A:72 [in LS2NF.grammar]
A:73 [in LS2NF.ambiguity]
A:74 [in LS2NF.sub_derive]
a:75 [in LS2NF.slice]
A:78 [in LS2NF.encoding]
a:79 [in LS2NF.slice]
a:8 [in LS2NF.witness]
A:8 [in LS2NF.derivation]
A:8 [in LS2NF.sub_derive]
a:81 [in LS2NF.slice]
A:81 [in LS2NF.sub_derive]
A:82 [in LS2NF.encoding]
a:84 [in LS2NF.slice]
A:85 [in LS2NF.sub_derive]
A:89 [in LS2NF.grammar]
A:9 [in LS2NF.util]
A:9 [in LS2NF.derivation]
A:91 [in LS2NF.encoding]
A:91 [in LS2NF.sub_derive]
A:92 [in LS2NF.grammar]
A:93 [in LS2NF.encoding]
A:96 [in LS2NF.grammar]
A:97 [in LS2NF.encoding]
B
Bl:107 [in LS2NF.sub_derive]Bl:113 [in LS2NF.sub_derive]
Bl:17 [in LS2NF.derivation]
Bl:30 [in LS2NF.derivation]
Bl:45 [in LS2NF.sub_derive]
Bl:51 [in LS2NF.sub_derive]
Bl:72 [in LS2NF.encoding]
Bl:86 [in LS2NF.sub_derive]
Bl:92 [in LS2NF.sub_derive]
Bl:97 [in LS2NF.grammar]
Br:109 [in LS2NF.sub_derive]
Br:115 [in LS2NF.sub_derive]
Br:18 [in LS2NF.derivation]
Br:31 [in LS2NF.derivation]
Br:46 [in LS2NF.sub_derive]
Br:52 [in LS2NF.sub_derive]
Br:73 [in LS2NF.encoding]
Br:88 [in LS2NF.sub_derive]
Br:94 [in LS2NF.sub_derive]
Br:98 [in LS2NF.grammar]
B':108 [in LS2NF.encoding]
B':113 [in LS2NF.encoding]
B':127 [in LS2NF.sub_derive]
B':131 [in LS2NF.sub_derive]
B':94 [in LS2NF.encoding]
B':98 [in LS2NF.encoding]
B:103 [in LS2NF.sub_derive]
B:104 [in LS2NF.encoding]
B:11 [in LS2NF.acyclic]
B:13 [in LS2NF.derivation]
B:137 [in LS2NF.encoding]
B:145 [in LS2NF.encoding]
B:15 [in LS2NF.acyclic]
B:28 [in LS2NF.ambiguity]
B:28 [in LS2NF.derivation]
B:41 [in LS2NF.sub_derive]
B:58 [in LS2NF.sub_derive]
B:62 [in LS2NF.sub_derive]
B:66 [in LS2NF.sub_derive]
B:70 [in LS2NF.encoding]
B:76 [in LS2NF.sub_derive]
B:8 [in LS2NF.acyclic]
B:82 [in LS2NF.sub_derive]
B:88 [in LS2NF.encoding]
B:93 [in LS2NF.grammar]
E
EqDecision0:118 [in LS2NF.grammar]EqDecision0:24 [in LS2NF.grammar]
EqDecision0:3 [in LS2NF.encoding]
EqDecision0:3 [in LS2NF.acyclic]
EqDecision0:3 [in LS2NF.witness]
EqDecision0:3 [in LS2NF.derivation]
EqDecision0:3 [in LS2NF.sub_derive]
EqDecision0:32 [in LS2NF.grammar]
EqDecision0:38 [in LS2NF.grammar]
EqDecision0:6 [in LS2NF.grammar]
EqDecision0:7 [in LS2NF.ambiguity]
EqDecision0:8 [in LS2NF.acyclic_wf]
EqDecision1:119 [in LS2NF.grammar]
EqDecision1:25 [in LS2NF.grammar]
EqDecision1:33 [in LS2NF.grammar]
EqDecision1:39 [in LS2NF.grammar]
EqDecision1:4 [in LS2NF.witness]
EqDecision1:4 [in LS2NF.derivation]
EqDecision1:4 [in LS2NF.sub_derive]
EqDecision1:5 [in LS2NF.encoding]
EqDecision1:8 [in LS2NF.ambiguity]
E:12 [in LS2NF.acyclic]
E:16 [in LS2NF.acyclic]
F
Finite0:18 [in LS2NF.acyclic]Finite0:6 [in LS2NF.encoding]
Finite0:9 [in LS2NF.acyclic_wf]
f:29 [in LS2NF.ambiguity]
G
G:127 [in LS2NF.grammar]G:4 [in LS2NF.acyclic]
G:5 [in LS2NF.witness]
G:5 [in LS2NF.derivation]
G:5 [in LS2NF.sub_derive]
G:7 [in LS2NF.encoding]
G:71 [in LS2NF.grammar]
G:84 [in LS2NF.grammar]
G:88 [in LS2NF.grammar]
G:9 [in LS2NF.ambiguity]
H
H:16 [in LS2NF.ambiguity]h:17 [in LS2NF.ambiguity]
H:218 [in LS2NF.encoding]
h:43 [in LS2NF.slice]
H:44 [in LS2NF.ambiguity]
h:45 [in LS2NF.ambiguity]
I
Inhabited0:4 [in LS2NF.encoding]i:12 [in LS2NF.util]
i:13 [in LS2NF.encoding]
i:18 [in LS2NF.util]
i:20 [in LS2NF.encoding]
i:21 [in LS2NF.slice]
i:25 [in LS2NF.encoding]
i:28 [in LS2NF.encoding]
i:29 [in LS2NF.encoding]
i:30 [in LS2NF.encoding]
i:49 [in LS2NF.slice]
i:58 [in LS2NF.encoding]
i:6 [in LS2NF.util]
J
j:13 [in LS2NF.util]j:50 [in LS2NF.slice]
K
k':47 [in LS2NF.slice]k':55 [in LS2NF.slice]
k1:34 [in LS2NF.slice]
k1:38 [in LS2NF.slice]
k1:60 [in LS2NF.slice]
k2:35 [in LS2NF.slice]
k2:39 [in LS2NF.slice]
k2:62 [in LS2NF.slice]
k:102 [in LS2NF.encoding]
k:11 [in LS2NF.slice]
k:118 [in LS2NF.encoding]
k:122 [in LS2NF.encoding]
k:128 [in LS2NF.encoding]
k:131 [in LS2NF.encoding]
k:134 [in LS2NF.encoding]
k:14 [in LS2NF.slice]
k:143 [in LS2NF.encoding]
k:161 [in LS2NF.encoding]
k:163 [in LS2NF.encoding]
k:165 [in LS2NF.encoding]
k:167 [in LS2NF.encoding]
k:169 [in LS2NF.encoding]
k:17 [in LS2NF.slice]
k:183 [in LS2NF.encoding]
k:19 [in LS2NF.encoding]
k:192 [in LS2NF.encoding]
k:20 [in LS2NF.slice]
k:216 [in LS2NF.encoding]
k:22 [in LS2NF.encoding]
k:22 [in LS2NF.util]
k:222 [in LS2NF.encoding]
k:225 [in LS2NF.encoding]
k:24 [in LS2NF.encoding]
k:27 [in LS2NF.slice]
k:31 [in LS2NF.slice]
k:4 [in LS2NF.slice]
k:42 [in LS2NF.slice]
k:44 [in LS2NF.encoding]
k:46 [in LS2NF.slice]
k:53 [in LS2NF.encoding]
k:53 [in LS2NF.slice]
k:56 [in LS2NF.encoding]
k:58 [in LS2NF.slice]
k:61 [in LS2NF.encoding]
k:64 [in LS2NF.encoding]
k:8 [in LS2NF.slice]
k:80 [in LS2NF.encoding]
k:82 [in LS2NF.slice]
k:85 [in LS2NF.slice]
k:86 [in LS2NF.encoding]
L
lhs:79 [in LS2NF.grammar]l':63 [in LS2NF.slice]
l':73 [in LS2NF.slice]
l1:188 [in LS2NF.encoding]
l1:65 [in LS2NF.slice]
l1:68 [in LS2NF.slice]
l1:71 [in LS2NF.slice]
l1:77 [in LS2NF.slice]
l1:86 [in LS2NF.slice]
l2:189 [in LS2NF.encoding]
l2:66 [in LS2NF.slice]
l2:69 [in LS2NF.slice]
l2:72 [in LS2NF.slice]
l2:78 [in LS2NF.slice]
l2:87 [in LS2NF.slice]
l:11 [in LS2NF.util]
l:12 [in LS2NF.slice]
l:15 [in LS2NF.slice]
l:17 [in LS2NF.util]
l:18 [in LS2NF.slice]
l:190 [in LS2NF.encoding]
l:2 [in LS2NF.slice]
l:21 [in LS2NF.util]
l:22 [in LS2NF.slice]
l:24 [in LS2NF.util]
l:25 [in LS2NF.slice]
l:26 [in LS2NF.util]
l:27 [in LS2NF.util]
l:29 [in LS2NF.slice]
l:32 [in LS2NF.slice]
l:36 [in LS2NF.slice]
l:40 [in LS2NF.slice]
l:44 [in LS2NF.slice]
l:48 [in LS2NF.slice]
l:5 [in LS2NF.slice]
l:51 [in LS2NF.slice]
l:56 [in LS2NF.slice]
l:64 [in LS2NF.slice]
l:67 [in LS2NF.slice]
l:7 [in LS2NF.slice]
l:70 [in LS2NF.slice]
l:74 [in LS2NF.slice]
l:76 [in LS2NF.slice]
l:79 [in LS2NF.encoding]
l:80 [in LS2NF.slice]
l:83 [in LS2NF.slice]
l:9 [in LS2NF.slice]
M
mx:30 [in LS2NF.ambiguity]m:103 [in LS2NF.encoding]
m:119 [in LS2NF.encoding]
m:136 [in LS2NF.encoding]
m:144 [in LS2NF.encoding]
m:162 [in LS2NF.encoding]
m:164 [in LS2NF.encoding]
m:166 [in LS2NF.encoding]
m:168 [in LS2NF.encoding]
m:170 [in LS2NF.encoding]
m:18 [in LS2NF.encoding]
m:184 [in LS2NF.encoding]
m:193 [in LS2NF.encoding]
m:21 [in LS2NF.encoding]
m:217 [in LS2NF.encoding]
m:223 [in LS2NF.encoding]
m:227 [in LS2NF.encoding]
m:23 [in LS2NF.encoding]
m:45 [in LS2NF.encoding]
m:54 [in LS2NF.encoding]
m:57 [in LS2NF.encoding]
m:62 [in LS2NF.encoding]
m:65 [in LS2NF.encoding]
m:81 [in LS2NF.encoding]
m:87 [in LS2NF.encoding]
N
n:1 [in LS2NF.util]N:102 [in LS2NF.grammar]
N:15 [in LS2NF.grammar]
N:2 [in LS2NF.ambiguity]
N:2 [in LS2NF.encoding]
N:2 [in LS2NF.acyclic]
N:2 [in LS2NF.witness]
N:2 [in LS2NF.derivation]
N:2 [in LS2NF.sub_derive]
N:23 [in LS2NF.grammar]
N:31 [in LS2NF.grammar]
N:37 [in LS2NF.grammar]
n:4 [in LS2NF.util]
n:5 [in LS2NF.util]
N:51 [in LS2NF.grammar]
N:60 [in LS2NF.grammar]
n:7 [in LS2NF.util]
N:70 [in LS2NF.grammar]
N:76 [in LS2NF.grammar]
N:82 [in LS2NF.grammar]
N:87 [in LS2NF.grammar]
P
pt1:8 [in LS2NF.grammar]pt2:9 [in LS2NF.grammar]
pt:107 [in LS2NF.grammar]
p:11 [in LS2NF.derivation]
p:133 [in LS2NF.grammar]
p:176 [in LS2NF.encoding]
P:191 [in LS2NF.encoding]
p:27 [in LS2NF.derivation]
p:41 [in LS2NF.grammar]
p:45 [in LS2NF.grammar]
p:83 [in LS2NF.grammar]
p:9 [in LS2NF.witness]
R
rhs:80 [in LS2NF.grammar]R:10 [in LS2NF.util]
r:105 [in LS2NF.grammar]
r:106 [in LS2NF.grammar]
r:108 [in LS2NF.grammar]
r:110 [in LS2NF.grammar]
R:2 [in LS2NF.acyclic_wf]
R:6 [in LS2NF.acyclic_wf]
S
S:101 [in LS2NF.encoding]S:117 [in LS2NF.encoding]
S:135 [in LS2NF.encoding]
S:142 [in LS2NF.encoding]
s:22 [in LS2NF.ambiguity]
S:26 [in LS2NF.encoding]
s:34 [in LS2NF.ambiguity]
s:37 [in LS2NF.ambiguity]
S:38 [in LS2NF.encoding]
s:40 [in LS2NF.ambiguity]
s:48 [in LS2NF.ambiguity]
S:85 [in LS2NF.encoding]
T
tk:24 [in LS2NF.sub_derive]tl:111 [in LS2NF.grammar]
tl:30 [in LS2NF.sub_derive]
token:63 [in LS2NF.grammar]
Transitive0:16 [in LS2NF.util]
tr':26 [in LS2NF.ambiguity]
tr:112 [in LS2NF.grammar]
tr:31 [in LS2NF.sub_derive]
t':12 [in LS2NF.sub_derive]
t':135 [in LS2NF.grammar]
t':15 [in LS2NF.sub_derive]
t':17 [in LS2NF.sub_derive]
t':19 [in LS2NF.sub_derive]
t':25 [in LS2NF.sub_derive]
t':28 [in LS2NF.sub_derive]
t':36 [in LS2NF.sub_derive]
T':41 [in LS2NF.ambiguity]
T':49 [in LS2NF.ambiguity]
t1':25 [in LS2NF.ambiguity]
t1':61 [in LS2NF.ambiguity]
t1':65 [in LS2NF.ambiguity]
t1':69 [in LS2NF.ambiguity]
t1:12 [in LS2NF.ambiguity]
t1:120 [in LS2NF.grammar]
t1:125 [in LS2NF.grammar]
t1:138 [in LS2NF.grammar]
t1:16 [in LS2NF.witness]
t1:178 [in LS2NF.encoding]
t1:18 [in LS2NF.ambiguity]
t1:197 [in LS2NF.encoding]
t1:211 [in LS2NF.encoding]
t1:213 [in LS2NF.encoding]
t1:3 [in LS2NF.ambiguity]
t1:52 [in LS2NF.ambiguity]
t1:57 [in LS2NF.ambiguity]
t1:59 [in LS2NF.ambiguity]
t1:63 [in LS2NF.ambiguity]
t1:67 [in LS2NF.ambiguity]
t2':62 [in LS2NF.ambiguity]
t2':66 [in LS2NF.ambiguity]
t2':70 [in LS2NF.ambiguity]
t2:121 [in LS2NF.grammar]
t2:126 [in LS2NF.grammar]
t2:13 [in LS2NF.ambiguity]
t2:139 [in LS2NF.grammar]
t2:17 [in LS2NF.witness]
t2:179 [in LS2NF.encoding]
t2:19 [in LS2NF.ambiguity]
t2:198 [in LS2NF.encoding]
t2:212 [in LS2NF.encoding]
t2:214 [in LS2NF.encoding]
t2:4 [in LS2NF.ambiguity]
t2:53 [in LS2NF.ambiguity]
t2:58 [in LS2NF.ambiguity]
t2:60 [in LS2NF.ambiguity]
t2:64 [in LS2NF.ambiguity]
t2:68 [in LS2NF.ambiguity]
t:109 [in LS2NF.grammar]
t:11 [in LS2NF.sub_derive]
t:113 [in LS2NF.grammar]
t:115 [in LS2NF.grammar]
t:12 [in LS2NF.witness]
t:14 [in LS2NF.sub_derive]
t:141 [in LS2NF.grammar]
t:146 [in LS2NF.grammar]
t:16 [in LS2NF.sub_derive]
t:177 [in LS2NF.encoding]
t:18 [in LS2NF.sub_derive]
t:199 [in LS2NF.encoding]
T:20 [in LS2NF.ambiguity]
t:20 [in LS2NF.sub_derive]
t:200 [in LS2NF.encoding]
t:209 [in LS2NF.encoding]
t:21 [in LS2NF.ambiguity]
t:210 [in LS2NF.encoding]
t:22 [in LS2NF.sub_derive]
t:27 [in LS2NF.sub_derive]
T:32 [in LS2NF.ambiguity]
t:33 [in LS2NF.ambiguity]
T:35 [in LS2NF.ambiguity]
t:36 [in LS2NF.ambiguity]
t:37 [in LS2NF.sub_derive]
T:38 [in LS2NF.ambiguity]
t:39 [in LS2NF.ambiguity]
T:46 [in LS2NF.ambiguity]
t:47 [in LS2NF.ambiguity]
t:9 [in LS2NF.sub_derive]
V
vl:68 [in LS2NF.sub_derive]vl:72 [in LS2NF.sub_derive]
vr:69 [in LS2NF.sub_derive]
vr:73 [in LS2NF.sub_derive]
v:59 [in LS2NF.sub_derive]
v:63 [in LS2NF.sub_derive]
v:67 [in LS2NF.sub_derive]
v:77 [in LS2NF.sub_derive]
W
wl:48 [in LS2NF.sub_derive]wl:54 [in LS2NF.sub_derive]
wr:49 [in LS2NF.sub_derive]
wr:55 [in LS2NF.sub_derive]
w':129 [in LS2NF.sub_derive]
w':133 [in LS2NF.sub_derive]
w1:108 [in LS2NF.sub_derive]
w1:114 [in LS2NF.sub_derive]
w1:20 [in LS2NF.derivation]
w1:33 [in LS2NF.derivation]
w1:46 [in LS2NF.grammar]
w1:87 [in LS2NF.sub_derive]
w1:93 [in LS2NF.sub_derive]
w2:110 [in LS2NF.sub_derive]
w2:116 [in LS2NF.sub_derive]
w2:18 [in LS2NF.witness]
w2:21 [in LS2NF.derivation]
w2:34 [in LS2NF.derivation]
w2:47 [in LS2NF.grammar]
w2:89 [in LS2NF.sub_derive]
w2:95 [in LS2NF.sub_derive]
w:104 [in LS2NF.sub_derive]
w:11 [in LS2NF.ambiguity]
w:121 [in LS2NF.encoding]
w:125 [in LS2NF.encoding]
w:127 [in LS2NF.encoding]
w:13 [in LS2NF.grammar]
w:13 [in LS2NF.witness]
w:130 [in LS2NF.encoding]
w:133 [in LS2NF.encoding]
w:143 [in LS2NF.grammar]
w:145 [in LS2NF.grammar]
w:15 [in LS2NF.ambiguity]
w:15 [in LS2NF.derivation]
w:226 [in LS2NF.encoding]
w:23 [in LS2NF.derivation]
w:25 [in LS2NF.derivation]
w:27 [in LS2NF.encoding]
w:36 [in LS2NF.derivation]
w:39 [in LS2NF.encoding]
w:43 [in LS2NF.ambiguity]
w:43 [in LS2NF.sub_derive]
w:51 [in LS2NF.ambiguity]
w:57 [in LS2NF.sub_derive]
w:60 [in LS2NF.encoding]
w:61 [in LS2NF.sub_derive]
w:63 [in LS2NF.encoding]
w:65 [in LS2NF.sub_derive]
w:72 [in LS2NF.ambiguity]
w:74 [in LS2NF.ambiguity]
w:75 [in LS2NF.sub_derive]
w:77 [in LS2NF.encoding]
w:83 [in LS2NF.sub_derive]
X
x1:49 [in LS2NF.encoding]x2:51 [in LS2NF.encoding]
x:110 [in LS2NF.encoding]
x:115 [in LS2NF.encoding]
X:120 [in LS2NF.encoding]
X:129 [in LS2NF.encoding]
X:132 [in LS2NF.encoding]
x:138 [in LS2NF.encoding]
x:14 [in LS2NF.util]
x:158 [in LS2NF.encoding]
x:171 [in LS2NF.encoding]
x:181 [in LS2NF.encoding]
x:19 [in LS2NF.util]
x:194 [in LS2NF.encoding]
x:219 [in LS2NF.encoding]
X:224 [in LS2NF.encoding]
x:24 [in LS2NF.slice]
x:25 [in LS2NF.util]
x:28 [in LS2NF.slice]
x:3 [in LS2NF.acyclic_wf]
x:31 [in LS2NF.ambiguity]
x:32 [in LS2NF.encoding]
x:35 [in LS2NF.encoding]
x:4 [in LS2NF.acyclic_wf]
x:42 [in LS2NF.encoding]
X:59 [in LS2NF.encoding]
x:67 [in LS2NF.encoding]
x:7 [in LS2NF.acyclic_wf]
X:76 [in LS2NF.encoding]
x:8 [in LS2NF.util]
x:83 [in LS2NF.encoding]
x:89 [in LS2NF.encoding]
Y
y:15 [in LS2NF.util]y:20 [in LS2NF.util]
y:5 [in LS2NF.acyclic_wf]
other
Σ:1 [in LS2NF.grammar]Σ:1 [in LS2NF.ambiguity]
Σ:1 [in LS2NF.encoding]
Σ:1 [in LS2NF.acyclic]
Σ:1 [in LS2NF.witness]
Σ:1 [in LS2NF.derivation]
Σ:1 [in LS2NF.sub_derive]
Σ:10 [in LS2NF.grammar]
Σ:101 [in LS2NF.grammar]
Σ:11 [in LS2NF.grammar]
Σ:12 [in LS2NF.grammar]
Σ:14 [in LS2NF.grammar]
Σ:22 [in LS2NF.grammar]
Σ:30 [in LS2NF.grammar]
Σ:36 [in LS2NF.grammar]
Σ:40 [in LS2NF.grammar]
Σ:42 [in LS2NF.grammar]
Σ:44 [in LS2NF.grammar]
Σ:48 [in LS2NF.grammar]
Σ:5 [in LS2NF.grammar]
Σ:50 [in LS2NF.grammar]
Σ:59 [in LS2NF.grammar]
Σ:69 [in LS2NF.grammar]
Σ:7 [in LS2NF.grammar]
Σ:75 [in LS2NF.grammar]
Σ:81 [in LS2NF.grammar]
Σ:86 [in LS2NF.grammar]
α:150 [in LS2NF.encoding]
α:26 [in LS2NF.grammar]
α:34 [in LS2NF.grammar]
α:73 [in LS2NF.grammar]
α:90 [in LS2NF.grammar]
β:27 [in LS2NF.grammar]
β:35 [in LS2NF.grammar]
δ':100 [in LS2NF.encoding]
δ':152 [in LS2NF.encoding]
δ':75 [in LS2NF.encoding]
δ':96 [in LS2NF.encoding]
δ1:50 [in LS2NF.encoding]
δ2:52 [in LS2NF.encoding]
δ:111 [in LS2NF.encoding]
δ:116 [in LS2NF.encoding]
δ:139 [in LS2NF.encoding]
δ:140 [in LS2NF.encoding]
δ:141 [in LS2NF.encoding]
δ:149 [in LS2NF.encoding]
δ:155 [in LS2NF.encoding]
δ:159 [in LS2NF.encoding]
δ:172 [in LS2NF.encoding]
δ:182 [in LS2NF.encoding]
δ:195 [in LS2NF.encoding]
δ:220 [in LS2NF.encoding]
δ:33 [in LS2NF.encoding]
δ:36 [in LS2NF.encoding]
δ:43 [in LS2NF.encoding]
δ:68 [in LS2NF.encoding]
δ:84 [in LS2NF.encoding]
δ:90 [in LS2NF.encoding]
σ1:32 [in LS2NF.sub_derive]
σ2:33 [in LS2NF.sub_derive]
σ:118 [in LS2NF.sub_derive]
σ:120 [in LS2NF.sub_derive]
σ:134 [in LS2NF.sub_derive]
σ:70 [in LS2NF.sub_derive]
σ:78 [in LS2NF.sub_derive]
σ:97 [in LS2NF.sub_derive]
σ:99 [in LS2NF.sub_derive]
τ:119 [in LS2NF.sub_derive]
τ:121 [in LS2NF.sub_derive]
τ:135 [in LS2NF.sub_derive]
τ:71 [in LS2NF.sub_derive]
τ:98 [in LS2NF.sub_derive]
φ':100 [in LS2NF.grammar]
φ':95 [in LS2NF.grammar]
φ:105 [in LS2NF.sub_derive]
φ:106 [in LS2NF.encoding]
φ:109 [in LS2NF.encoding]
φ:11 [in LS2NF.witness]
φ:111 [in LS2NF.sub_derive]
φ:114 [in LS2NF.encoding]
φ:117 [in LS2NF.sub_derive]
φ:123 [in LS2NF.encoding]
φ:124 [in LS2NF.encoding]
φ:125 [in LS2NF.sub_derive]
φ:126 [in LS2NF.encoding]
φ:128 [in LS2NF.sub_derive]
φ:13 [in LS2NF.acyclic]
φ:132 [in LS2NF.sub_derive]
φ:136 [in LS2NF.grammar]
φ:14 [in LS2NF.derivation]
φ:140 [in LS2NF.grammar]
φ:15 [in LS2NF.witness]
φ:17 [in LS2NF.acyclic]
φ:19 [in LS2NF.derivation]
φ:29 [in LS2NF.derivation]
φ:32 [in LS2NF.derivation]
φ:41 [in LS2NF.encoding]
φ:42 [in LS2NF.sub_derive]
φ:43 [in LS2NF.grammar]
φ:47 [in LS2NF.sub_derive]
φ:48 [in LS2NF.encoding]
φ:49 [in LS2NF.grammar]
φ:53 [in LS2NF.sub_derive]
φ:65 [in LS2NF.grammar]
φ:68 [in LS2NF.grammar]
φ:71 [in LS2NF.encoding]
φ:74 [in LS2NF.encoding]
φ:84 [in LS2NF.sub_derive]
φ:9 [in LS2NF.acyclic]
φ:90 [in LS2NF.sub_derive]
φ:92 [in LS2NF.encoding]
φ:94 [in LS2NF.grammar]
φ:95 [in LS2NF.encoding]
φ:96 [in LS2NF.sub_derive]
φ:99 [in LS2NF.grammar]
φ:99 [in LS2NF.encoding]
ψ1:185 [in LS2NF.encoding]
ψ2:186 [in LS2NF.encoding]
ψ:153 [in LS2NF.encoding]
ψ:157 [in LS2NF.encoding]
ψ:174 [in LS2NF.encoding]
ψ:201 [in LS2NF.encoding]
ψ:202 [in LS2NF.encoding]
ψ:203 [in LS2NF.encoding]
ψ:204 [in LS2NF.encoding]
ψ:205 [in LS2NF.encoding]
ψ:206 [in LS2NF.encoding]
ψ:207 [in LS2NF.encoding]
ψ:208 [in LS2NF.encoding]
Variable Index
E
encoding.Φ_app₂_spec [in LS2NF.encoding]encoding.Φ_app₂ [in LS2NF.encoding]
encoding.Φ_app₁_spec [in LS2NF.encoding]
encoding.Φ_app₁ [in LS2NF.encoding]
Library Index
A
acyclicacyclic_wf
ambiguity
D
derivationE
encodingG
grammarS
slicesub_derive
U
utilW
witnessLemma Index
A
acyclic_wf [in LS2NF.acyclic_wf]acyclic_flip_wf [in LS2NF.acyclic_wf]
acyclic_succ_wf [in LS2NF.acyclic]
acyclic_prec_wf [in LS2NF.acyclic]
apply_binary_nil_r [in LS2NF.encoding]
apply_binary_nil_l [in LS2NF.encoding]
apply_unary_nil [in LS2NF.encoding]
app_length_le_l [in LS2NF.encoding]
B
binary_clause_predicate_unique [in LS2NF.grammar]bind_Some_is_Some [in LS2NF.ambiguity]
C
check_tree_eq_spec [in LS2NF.grammar]check_lf_clause_eq_spec [in LS2NF.grammar]
check_derive_spec [in LS2NF.derivation]
check_reachable_from_spec [in LS2NF.sub_derive]
child_valid [in LS2NF.sub_derive]
D
decode_encode [in LS2NF.encoding]decode_lookup [in LS2NF.encoding]
decode_length [in LS2NF.encoding]
derivation_spec [in LS2NF.derivation]
derive_amb_iff_local_amb [in LS2NF.ambiguity]
derive_amb_implies_local_amb [in LS2NF.ambiguity]
diff_result_subtree [in LS2NF.ambiguity]
diff_result_not_similar [in LS2NF.ambiguity]
diff_Some_inv [in LS2NF.ambiguity]
diff_None [in LS2NF.ambiguity]
E
elem_of_clauses [in LS2NF.grammar]elem_of_choice_clauses [in LS2NF.encoding]
H
HdRel_Forall [in LS2NF.util]I
index_range_elem_of [in LS2NF.util]index_range_lookup [in LS2NF.util]
index_range_length [in LS2NF.util]
L
list_nonempty_length [in LS2NF.encoding]local_amb_implies_derive_amb [in LS2NF.ambiguity]
M
monotone_trans_alt_spec [in LS2NF.util]N
NoDup_lookup_in_range [in LS2NF.slice]R
reachable_from_spec [in LS2NF.sub_derive]reachable_to_spec [in LS2NF.sub_derive]
reachable_sublist [in LS2NF.sub_derive]
reachable_sub_sig [in LS2NF.sub_derive]
reachable_spec [in LS2NF.sub_derive]
replace_subtree [in LS2NF.ambiguity]
replace_witness [in LS2NF.ambiguity]
replace_id [in LS2NF.ambiguity]
replace_Some [in LS2NF.ambiguity]
S
similar_refl [in LS2NF.ambiguity]slice_app_inv_NoDup [in LS2NF.slice]
slice_sublist [in LS2NF.slice]
slice_app_inv_NoDup_aux [in LS2NF.slice]
slice_eq_inv_NoDup [in LS2NF.slice]
slice_eq_inv [in LS2NF.slice]
slice_split [in LS2NF.slice]
slice_app_2 [in LS2NF.slice]
slice_app_1 [in LS2NF.slice]
slice_full_iff [in LS2NF.slice]
slice_singleton_iff [in LS2NF.slice]
slice_singleton [in LS2NF.slice]
slice_lookup [in LS2NF.slice]
slice_nonempty_iff [in LS2NF.slice]
slice_nil_iff [in LS2NF.slice]
slice_length [in LS2NF.slice]
slice_full [in LS2NF.slice]
slice_nil [in LS2NF.slice]
Sorted_monotone [in LS2NF.util]
Sorted_cons_iff [in LS2NF.util]
step_sub [in LS2NF.sub_derive]
step_spec [in LS2NF.sub_derive]
sublist_app_slice_NoDup [in LS2NF.slice]
sublist_slice [in LS2NF.slice]
sublist_app_r [in LS2NF.slice]
sublist_app_l [in LS2NF.slice]
subtree_binary_inv [in LS2NF.sub_derive]
subtree_unary_inv [in LS2NF.sub_derive]
subtree_token_inv [in LS2NF.sub_derive]
subtree_ε_inv [in LS2NF.sub_derive]
subtree_valid [in LS2NF.sub_derive]
T
tc_flip [in LS2NF.acyclic_wf]tc_refl_ex_loop [in LS2NF.acyclic_wf]
U
unary_clause_predicate_unique [in LS2NF.grammar]W
well_formed_no_dup [in LS2NF.encoding]witness_binary [in LS2NF.witness]
witness_unary [in LS2NF.witness]
witness_atom [in LS2NF.witness]
witness_ε [in LS2NF.witness]
wrap_with_id [in LS2NF.encoding]
other
Φ_amb_complete [in LS2NF.encoding]Φ_amb_sound [in LS2NF.encoding]
Φ_multi_spec [in LS2NF.encoding]
Φ_choice_sem_witness [in LS2NF.encoding]
Φ_reach_empty_spec [in LS2NF.encoding]
Φ_reach_nonempty_spec [in LS2NF.encoding]
Φ_reach_sat [in LS2NF.encoding]
Φ_reach_empty_sat [in LS2NF.encoding]
Φ_reach_nonempty_sat [in LS2NF.encoding]
Φ_derive_spec [in LS2NF.encoding]
Φ_derive_sat [in LS2NF.encoding]
Φ_well_formed_spec [in LS2NF.encoding]
Φ_well_formed_sat [in LS2NF.encoding]
Constructor Index
A
atom [in LS2NF.grammar]B
binary [in LS2NF.grammar]binary_tree [in LS2NF.grammar]
C
child_right [in LS2NF.sub_derive]child_left [in LS2NF.sub_derive]
child_unary [in LS2NF.sub_derive]
D
derive_binary [in LS2NF.derivation]derive_unary [in LS2NF.derivation]
derive_atom [in LS2NF.derivation]
derive_ε [in LS2NF.derivation]
L
lf_binary [in LS2NF.grammar]lf_unary [in LS2NF.grammar]
lf_atom [in LS2NF.grammar]
lf_ε [in LS2NF.grammar]
M
mk_production [in LS2NF.grammar]R
reachable_from_right [in LS2NF.sub_derive]reachable_from_left [in LS2NF.sub_derive]
reachable_from_unary [in LS2NF.sub_derive]
reachable_from_refl [in LS2NF.sub_derive]
reachable_to_right [in LS2NF.sub_derive]
reachable_to_left [in LS2NF.sub_derive]
reachable_to_unary [in LS2NF.sub_derive]
reachable_to_refl [in LS2NF.sub_derive]
S
step_right [in LS2NF.sub_derive]step_left [in LS2NF.sub_derive]
step_unary [in LS2NF.sub_derive]
succ_right [in LS2NF.acyclic]
succ_left [in LS2NF.acyclic]
succ_unary [in LS2NF.acyclic]
T
token_tree [in LS2NF.grammar]U
unary [in LS2NF.grammar]unary_tree [in LS2NF.grammar]
using_binary [in LS2NF.encoding]
using_unary [in LS2NF.encoding]
using_atom [in LS2NF.encoding]
using_ε [in LS2NF.encoding]
V
valid_binary [in LS2NF.grammar]valid_unary [in LS2NF.grammar]
valid_token [in LS2NF.grammar]
valid_ε [in LS2NF.grammar]
other
ε [in LS2NF.grammar]ε_tree [in LS2NF.grammar]
Inductive Index
C
child [in LS2NF.sub_derive]choice_clause [in LS2NF.encoding]
clause [in LS2NF.grammar]
D
derivation [in LS2NF.derivation]L
lf_clause [in LS2NF.grammar]P
production [in LS2NF.grammar]R
reachable_from [in LS2NF.sub_derive]reachable_to [in LS2NF.sub_derive]
S
step [in LS2NF.sub_derive]succ [in LS2NF.acyclic]
T
tree [in LS2NF.grammar]tree_valid [in LS2NF.grammar]
Projection Index
B
binary_clause_predicate [in LS2NF.grammar]C
can_reach_from [in LS2NF.encoding]can_derive [in LS2NF.encoding]
col [in LS2NF.encoding]
L
lf_clauses_no_dup [in LS2NF.grammar]lf_clauses [in LS2NF.grammar]
line [in LS2NF.encoding]
line_col [in LS2NF.encoding]
P
pos [in LS2NF.grammar]S
start [in LS2NF.grammar]T
term [in LS2NF.encoding]token [in LS2NF.grammar]
U
unary_clause_predicate [in LS2NF.grammar]other
ε_can_reach_from [in LS2NF.encoding]Section Index
A
acyclic [in LS2NF.acyclic]acyclic_wf [in LS2NF.acyclic_wf]
ambiguity [in LS2NF.ambiguity]
C
clauses [in LS2NF.grammar]D
derivation [in LS2NF.derivation]E
encoding [in LS2NF.encoding]P
parsing [in LS2NF.grammar]S
slice [in LS2NF.slice]Sorted_lemmas [in LS2NF.util]
sub_derive [in LS2NF.sub_derive]
W
witness [in LS2NF.witness]Instance Index
L
lf_clause_eq_dec [in LS2NF.grammar]P
pos_token_lt_trans [in LS2NF.grammar]pos_token_eq_dec [in LS2NF.grammar]
production_elem_of_grammar [in LS2NF.grammar]
S
sub_derive_trans [in LS2NF.sub_derive]T
tree_eq_dec [in LS2NF.grammar]Definition Index
A
acyclic [in LS2NF.acyclic]app₁ [in LS2NF.grammar]
app₂ [in LS2NF.grammar]
B
binary_predicate [in LS2NF.grammar]C
check_tree_eq [in LS2NF.grammar]check_lf_clause_eq [in LS2NF.grammar]
check_derive [in LS2NF.derivation]
check_reachable_from [in LS2NF.sub_derive]
choice_clauses [in LS2NF.encoding]
clauses [in LS2NF.grammar]
D
decode [in LS2NF.encoding]derive [in LS2NF.grammar]
derive_amb [in LS2NF.ambiguity]
diff [in LS2NF.ambiguity]
E
encode [in LS2NF.encoding]F
formula [in LS2NF.encoding]I
index_range [in LS2NF.util]L
local_amb [in LS2NF.ambiguity]M
monotone [in LS2NF.util]monotone_trans_alt [in LS2NF.util]
P
pos_token_lt [in LS2NF.grammar]prec [in LS2NF.acyclic]
R
reachable [in LS2NF.sub_derive]rel_acyclic [in LS2NF.acyclic_wf]
replace [in LS2NF.ambiguity]
root [in LS2NF.grammar]
S
sentence [in LS2NF.grammar]sig [in LS2NF.sub_derive]
similar [in LS2NF.ambiguity]
slice [in LS2NF.slice]
sublist [in LS2NF.slice]
subtree [in LS2NF.sub_derive]
sub_derive [in LS2NF.sub_derive]
T
tree_witness [in LS2NF.grammar]U
unary_predicate [in LS2NF.grammar]W
well_formed [in LS2NF.grammar]word [in LS2NF.grammar]
other
Φ_amb [in LS2NF.encoding]Φ_multi [in LS2NF.encoding]
Φ_choice_sem [in LS2NF.encoding]
Φ_reach [in LS2NF.encoding]
Φ_reach_empty [in LS2NF.encoding]
Φ_reach_nonempty [in LS2NF.encoding]
Φ_derive [in LS2NF.encoding]
Φ_well_formed [in LS2NF.encoding]
Record Index
G
grammar [in LS2NF.grammar]M
model [in LS2NF.encoding]P
pos_token [in LS2NF.grammar]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (955 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (704 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |