Minimal.Reduction.Parallel.Definition

inductive Premise {lst : List Attr} (l1 l2 : Bindings lst) :

nil : Premise Record.nil Record.nil
consVoid (a : Attr) {lst : List Attr} {l1 l2 : Bindings lst} {not_in : ¬a ∈ lst} : Premise l1 l2 → Premise (Record.cons a not_in none l1) (Record.cons a not_in none l2)
consAttached (a : Attr) (t1 t2 : Term) : (t1 ⇛ t2) → {lst : List Attr} → {l1 l2 : Bindings lst} → {not_in : ¬a ∈ lst} → Premise l1 l2 → Premise (Record.cons a not_in (some t1) l1) (Record.cons a not_in (some t2) l2)

Instances For

inductive PReduce :

Parallel reduction [KS22, Fig. 2]

pcongOBJ {lst : List Attr} (l newAttrs : Bindings lst) : Premise l newAttrs → (Term.obj l ⇛ Term.obj newAttrs)
pcong_ρ (n : Nat) : Term.loc n ⇛ Term.loc n
pcongDOT (t t' : Term) (a : Attr) : (t ⇛ t') → (t.dot a ⇛ t'.dot a)
pcongAPP (t t' u u' : Term) (a : Attr) : (t ⇛ t') → (u ⇛ u') → (t.app a u ⇛ t'.app a u')
pdot_c {t t' : Term} (t_c : Term) (c : Attr) {lst : List Attr} (l : Bindings lst) : (t ⇛ t') → t' = Term.obj l → lookup l c = some (some t_c) → (t.dot c ⇛ substitute (0, t') t_c)
pdot_cφ {t t' : Term} (c : Attr) {lst : List Attr} (l : Bindings lst) : (t ⇛ t') → t' = Term.obj l → lookup l c = none → "φ" ∈ lst → (t.dot c ⇛ (t'.dot "φ").dot c)
papp_c {t t' u u' : Term} (c : Attr) {lst : List Attr} (l : Bindings lst) : (t ⇛ t') → (u ⇛ u') → t' = Term.obj l → lookup l c = some none → (t.app c u ⇛ Term.obj (insert_φ l c (some (incLocators u'))))