Auxilary properties of parallel reduction

def reflexivePremise {lst : List Attr} (l : Bindings lst) : Premise l l

Equations

• reflexivePremise Record.nil = Premise.nil
• reflexivePremise (Record.cons name not_in none tail) = Premise.consVoid name (reflexivePremise tail)
• reflexivePremise (Record.cons name not_in (some t) tail) = Premise.consAttached name t t (prefl t) (reflexivePremise tail)

def prefl (t : Term) : t ⇛ t

Reflexivity of parallel reduction [KS22, Proposition 3.3]

Equations

• prefl (Term.loc n) = PReduce.pcong_ρ n
• prefl (t.dot a) = PReduce.pcongDOT t t a (prefl t)
• prefl (t.app a u) = PReduce.pcongAPP t t u u a (prefl t) (prefl u)
• prefl (Term.obj l) = PReduce.pcongOBJ l l (reflexivePremise l)

def singlePremise {lst : List Attr} (l : Bindings lst) (a : Attr) (t t' : Term) (isAttached : IsAttached a t l) (preduce : t ⇛ t') : Premise l (insert_φ l a (some t'))

Equations

• One or more equations did not get rendered due to their size.
• singlePremise Record.nil a t t' isAttached_3 preduce = Premise.nil
• singlePremise (Record.cons b not_in (some t) tail) b t t' (IsAttached.zeroth_attached b not_in t tail) preduce = ⋯.mpr (Premise.consAttached b t t' preduce (reflexivePremise tail))

def singlePremiseInsert {lst : List Attr} {l1 l2 : Bindings lst} {a : Attr} {t1 t2 : Term} (preduce : t1 ⇛ t2) (premise : Premise l1 l2) : Premise (insert_φ l1 a (some t1)) (insert_φ l2 a (some t2))

Equations

• One or more equations did not get rendered due to their size.
• singlePremiseInsert preduce Premise.nil = Premise.nil
• singlePremiseInsert preduce (Premise.consVoid b tail) = if eq : b = a then ⋯.mpr (Premise.consAttached b t1 t2 preduce tail) else ⋯.mpr (Premise.consVoid b (singlePremiseInsert preduce tail))

theorem lookup_void_premise {lst : List Attr} {l1 l2 : Bindings lst} {a : Attr} (lookup_void : lookup l1 a = some none) (premise : Premise l1 l2) : lookup l2 a = some none

def lookup_attached_premise {lst : List Attr} {l1 l2 : Bindings lst} {a : Attr} {u : Term} (lookup_attached : lookup l1 a = some (some u)) (premise : Premise l1 l2) : (u' : Term) × lookup l2 a = some (some u') ×' (u ⇛ u')

Equations

• One or more equations did not get rendered due to their size.
• lookup_attached_premise lookup_attached_3 Premise.nil = ⋯.mpr (Option.noConfusion lookup_attached_3)
• lookup_attached_premise lookup_attached_3 (Premise.consVoid b premise_tail) = ⋯.mpr (if eq : b = a then ⋯.elim else ⋯.mpr (lookup_attached_premise ⋯ premise_tail))

def preduce_incLocatorsFrom {t t' : Term} (i : Nat) : (t ⇛ t') → (incLocatorsFrom i t ⇛ incLocatorsFrom i t')

Increment of locators preserves parallel reduction.

Equations

• One or more equations did not get rendered due to their size.
• preduce_incLocatorsFrom i (PReduce.pcong_ρ n) = prefl (incLocatorsFrom i (Term.loc n))
• preduce_incLocatorsFrom i (PReduce.pcongDOT t_2 t'_2 a tt') = id (PReduce.pcongDOT (incLocatorsFrom i t_2) (incLocatorsFrom i t'_2) a (preduce_incLocatorsFrom i tt'))
• preduce_incLocatorsFrom i (PReduce.pdot_c t_c c l ss' eq lookup_eq) = ⋯.mpr (PReduce.pdot_c (incLocatorsFrom (i + 1) t_c) c (incLocatorsFromLst (i + 1) l) (preduce_incLocatorsFrom i ss') ⋯ ⋯)
• preduce_incLocatorsFrom i (PReduce.pdot_cφ c l ss' eq lookup_eq is_attr) = id (PReduce.pdot_cφ c (incLocatorsFromLst (i + 1) l) (preduce_incLocatorsFrom i ss') ⋯ ⋯ is_attr)

def preduce_incLocatorsFrom_Lst {lst : List Attr} {bnds bnds' : Bindings lst} (i : Nat) (premise : Premise bnds bnds') : Premise (incLocatorsFromLst (i + 1) bnds) (incLocatorsFromLst (i + 1) bnds')

Equations

• One or more equations did not get rendered due to their size.
• preduce_incLocatorsFrom_Lst i premise_3 = id Premise.nil
• preduce_incLocatorsFrom_Lst i (Premise.consVoid head tail) = id (Premise.consVoid head (preduce_incLocatorsFrom_Lst i tail))