MatchingLogic.BoxesControl

Coordinates exclude constants (Definition 2).

theorem MatchingLogic.BoxesControl.coord_arity_pos (S : Signature) (e : Coord S) : 1 ≤ S.arity e.fst

Every coordinate has arity at least one.

@[reducible, inline]

abbrev MatchingLogic.BoxesControl.Sg : Signature

One binary symbol.

Equations

• MatchingLogic.BoxesControl.Sg = { Sym := Unit, arity := fun (x : Unit) => 2 }

@[reducible, inline]

abbrev MatchingLogic.BoxesControl.SgConst : Signature

A signature of constants only.

Equations

• MatchingLogic.BoxesControl.SgConst = { Sym := Unit, arity := fun (x : Unit) => 0 }

theorem MatchingLogic.BoxesControl.coord_isEmpty_of_const : IsEmpty (Coord SgConst)

A constants-only signature has no coordinates at all, so E* = {ε}.

theorem MatchingLogic.BoxesControl.boxes_const (p : List (Coord SgConst)) (ψ : Pattern SgConst ℕ) : boxes p ψ = ψ

Consequently boxing is trivial there: the only word is ε.

A model in which position and order are visible.

0 ∈ f(1,1) and 1 ∈ f(2,3), so from 0 the first argument leads to 1 and so does the second, while from 1 the first argument leads to 2 and the second to 3. The two coordinates therefore separate after one step.

@[reducible, inline]

abbrev MatchingLogic.BoxesControl.Mo : Model Sg

The four-point model that distinguishes the two argument positions.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MatchingLogic.BoxesControl.e0 : Coord Sg

First coordinate of the binary symbol.

Equations

• MatchingLogic.BoxesControl.e0 = ⟨(), 0⟩

@[reducible, inline]

abbrev MatchingLogic.BoxesControl.e1 : Coord Sg

Second coordinate of the binary symbol.

Equations

• MatchingLogic.BoxesControl.e1 = ⟨(), 1⟩

theorem MatchingLogic.BoxesControl.dia_position_visible : Mo.denote (fun (x : ℕ) => 2) (dia e0 (Pattern.var 0)) ≠ Mo.denote (fun (x : ℕ) => 2) (dia e1 (Pattern.var 0))

A position swap in dia is observable. If dia put its argument in the wrong slot, this would fail.

theorem MatchingLogic.BoxesControl.reachWord_order_left (v : Fin 4) : Mo.reachWord [e0, e1] 0 v ↔ v = 3

The order of a word is observable, one way …

theorem MatchingLogic.BoxesControl.reachWord_order_right (v : Fin 4) : Mo.reachWord [e1, e0] 0 v ↔ v = 2

… and the other. Together these two force the composition order of reachWord, and through Lemma 4 the nesting order of boxes.