User:Timofonic/test3

Failed to parse (syntax error): {\displaystyle \text{first}: && \Node \to S \\ \text{first}: && \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto s \\ \\ \text{second}: && Node \to V \\ \text{second}: && \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto v \\ \\ \text{word}: && Node \to \Gamma \\ \text{word}: \tuple{s, v, \gamma} \mapsto \gamma \\ \\ \text{children}: && \Node \to \Node* \\ \text{children}: \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto \{ m | \forall m.m\in\{ n_{0}, n_{1} \ldots n_{i} \} \land m\in Node \} \\ \\ \text{all\_children}: && \Node \to \Node* \\ \text{all\_children}: n \mapsto \text{children}(n) \cup \{ m \docbooktolatexpipe{} \exists l.l \in\text{all\_children}(n).m\in l \} \\ \\ \text{is\_word} : && \Node \to B \\ \text{is\_word} : \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} = \Btt \iff (i = 0) \land n_{0} \in \Gamma \\ \text{contains\_word}: && \Node \times S \times \Gamma \to B contains\_word(n, s, \gamma) = tt \gamma = 0xfff\label{id2519386}\begingroup\catcode`\#=12\footnote{ %This is the so-called "anyword". Words with a word group of 0xfff match any other word. %}\endgroup\docbooktolatexmakefootnoteref{id2519386} \lor (\iff \exists m.m\in\text{all\_children}(n).(s = \text{second}(m)) \land (\text{is\_word}(m) \land (\text{word}(m) = \gamma))) \\ \text{verify\_sentence\_part\_elements}: && \Node \times \Node \to B \\ \text{verify\_sentence\_part\_elements}: && \tuple{n_{p}, n_{s}} \mapsto \Btt \iff (\text{first}(n_{s} = 152) \land ((\forall m.m \in \Node.\text{verify\_sentence\_part\_elements}(m, n_{s}) \iff \{ w \docbooktolatexpipe{} \exists t.t \in \text{all\_children}(m).w = \text{word}(t)\} = \emptyset) \lor \exists m \in \text{children}(n_{s}).\text{verify\_sentence\_part\_elements}(m, n_{s})) ) \lor ((\text{second}(n_{s}) = 153) \land (\exists m.m \in \text{children}(n_{s}).(\exists o \in \text{all\_children}(n_{s}).(\text{first}(o) = \text{first}(n_{p})) \land \text{word}(o) = \text{word}(m))) ) \lor ((\text{second}(n_{s}) \in \{144, 14c\}) \land (\exists m.m \in \text{children}(n_{s}).verify\_sentence\_part(m, n_{s}))) \\ \\ \text{verify\_sentence\_part}: && \Node \times \Node \to B \\ \text{verify\_sentence\_part}: && \tuple{n_{p}, n_{s}} \mapsto \Btt \iff \forall n.n \in \text{children}(n_{s}):\exists m.m\in\text{children}(n_{p}).(\text{first}(m) = \text{first}(n)) \land \text{verify\_sentence\_part\_elements}(n, m) \\ \\ \text{verify\_sentence\_part\_brackets}: && \Node \times \Node \to B \\ \text{verify\_sentence\_part\_brackets}: && \tuple{n_{p}, n_{s}} \mapsto \Btt \iff (\text{first}(n_{p}) = 152 \land (\forall m.m\in \Node.(\text{first}(m) = \text{first}(n_{s})) \land (\text{second}(m) = \text{second}(n_{s})). \text{verify\_sentence\_part}(n_{p}, m) \iff \{ w \docbooktolatexpipe{} \exists t.t \in \text{all\_children}(m).w = \text{word}(t)\} = \emptyset)) \lor ((\text{first}(n_{p}) \in \{141, 142, 143\}) \land \text{verify\_sentence\_part}(n_{p}, n_{s})) \\ }