Minimal.Reduction.Regular.Definition

inductive Reduce :

Evaluation [KS22, Fig. 1]

congOBJ {t t' : Term} (b : Attr) {lst : List Attr} (l : Bindings lst) : (t ⇝ t') → IsAttached b t l → (Term.obj l ⇝ Term.obj (insert_φ l b (some t')))
congDOT (t t' : Term) (a : Attr) : (t ⇝ t') → (t.dot a ⇝ t'.dot a)
congAPPₗ (t t' u : Term) (a : Attr) : (t ⇝ t') → (t.app a u ⇝ t'.app a u)
congAPPᵣ (t u u' : Term) (a : Attr) : (u ⇝ u') → (t.app a u ⇝ t.app a u')
dot_c {t : Term} (t_c : Term) (c : Attr) {lst : List Attr} (l : Bindings lst) : t = Term.obj l → lookup l c = some (some t_c) → (t.dot c ⇝ substitute (0, t) t_c)
dot_cφ {t : Term} (c : Attr) {lst : List Attr} (l : Bindings lst) : t = Term.obj l → lookup l c = none → "φ" ∈ lst → (t.dot c ⇝ (t.dot "φ").dot c)
app_c (t u : Term) (c : Attr) {lst : List Attr} (l : Bindings lst) : t = Term.obj l → lookup l c = some none → (t.app c u ⇝ Term.obj (insert_φ l c (some (incLocators u))))