Docs / Syntax / Minimalist / SyntacticObject / TokenCCommand

C-command between tokens on ordered trees

import Linglib.Syntax.Minimalist.SyntacticObject.TokenCCommand · namespace Minimalist.LinearizedSyntacticObject

This file reads c-command between two tokens off an ordered tree of vertices, by recursion on the tree: a token c-commands another when it is a daughter whose sister holds the other. The recursion needs no licensing, so it applies to the raw trees that recursions over a marked object produce. Between distinct tokens of a linearized object it is CCommands.

Main definitions

Minimalist.LinearizedSyntacticObject.Holds: the tree has a token as a leaf.
Minimalist.LinearizedSyntacticObject.TokenCCommands: c-command between tokens.

Declarations

The tree holds the token y.

def Holds L31–33

(y : LexicalItem.Token) (p : RoseTree SyntacticObject.Vertex) :

Holds y p = (Sum.inl (some y) ∈ p.leaves)

Used by instDecidablePredRoseTreeVertexTokenHolds, holds_leaf, holds_pair, holds_node_of_mem, exists_mem_of_holds_map, holds_of_mem_subtrees, holds_congr, TokenCCommands, tokenCCommands_pair_iff, TokenCCommands.holds, coe_mem_terms_iff, holds_iff_mem_yield, exists_holds

Used in Syntax/Minimalist/Copy/Reading

x c-commands y in an ordered tree: x is a daughter whose sister holds y.

inductive TokenCCommands L85–90

(x y : LexicalItem.Token) :

RoseTree SyntacticObject.Vertex → Prop

inl {x y : LexicalItem.Token} {a : SyntacticObject.Vertex} {l r : RoseTree SyntacticObject.Vertex} : TokenCCommands x y l → TokenCCommands x y (RoseTree.node a [l, r])
inr {x y : LexicalItem.Token} {a : SyntacticObject.Vertex} {l r : RoseTree SyntacticObject.Vertex} : TokenCCommands x y r → TokenCCommands x y (RoseTree.node a [l, r])
left {x y : LexicalItem.Token} {a : SyntacticObject.Vertex} {r : RoseTree SyntacticObject.Vertex} : Holds y r → TokenCCommands x y (RoseTree.node a [RoseTree.node (Sum.inl (some x)) [], r])
right {x y : LexicalItem.Token} {a : SyntacticObject.Vertex} {l : RoseTree SyntacticObject.Vertex} : Holds y l → TokenCCommands x y (RoseTree.node a [l, RoseTree.node (Sum.inl (some x)) []])

Built from

Used by tokenCCommands_pair_iff, not_tokenCCommands_of_length_ne, TokenCCommands.swap, TokenCCommands.holds, TokenCCommands.of_mem_subtrees, cCommands_iff_tokenCCommands

Used in Syntax/Minimalist/Copy/Reading

On a syntactic object c-command between distinct tokens is TokenCCommands.

theorem cCommands_iff_tokenCCommands L187–240

{x y : LexicalItem.Token} (hxy : x ≠ y) (p : LinearizedSyntacticObject) :

(↑p).CCommands ↑x ↑y ↔ TokenCCommands x y ↑p

Built from