Equivalence of ⇛ and ⇝

def reg_to_par {t t' : Term} : (t ⇝ t') → (t ⇛ t')

Equivalence of ⇛ and ⇝ [KS22, Proposition 3.4 (1)]

Equations

• reg_to_par (Reduce.congOBJ b l red isAttached) = PReduce.pcongOBJ l (insert_φ l b (some t'_2)) (singlePremise l b t_2 t'_2 isAttached (reg_to_par red))
• reg_to_par (Reduce.congDOT t_2 t'_2 a red) = PReduce.pcongDOT t_2 t'_2 a (reg_to_par red)
• reg_to_par (Reduce.congAPPₗ t_2 t'_2 u a red) = PReduce.pcongAPP t_2 t'_2 u u a (reg_to_par red) (prefl u)
• reg_to_par (Reduce.congAPPᵣ t_2 u u' a red) = PReduce.pcongAPP t_2 t_2 u u' a (prefl t_2) (reg_to_par red)
• reg_to_par (Reduce.dot_c t_c c l eq lookup_eq) = PReduce.pdot_c t_c c l (prefl t_2) eq lookup_eq
• reg_to_par (Reduce.dot_cφ c l eq lookup_c isAttr_φ) = PReduce.pdot_cφ c l (prefl t_2) eq lookup_c isAttr_φ
• reg_to_par (Reduce.app_c t_2 u c l eq lookup_eq) = PReduce.papp_c c l (prefl t_2) (prefl u) eq lookup_eq

def red_trans {t t' t'' : Term} (fi : t ⇝* t') (se : t' ⇝* t'') : t ⇝* t''

Transitivity of ⇝* [KS22, Lemma A.3]

Equations

• red_trans fi se = ReflTransGen.trans fi se

def consBindingsRedMany {lst : List Attr} (a : Attr) {not_in_a : ¬a ∈ lst} (u_a : Option Term) {l1 l2 : Bindings lst} (reds : Term.obj l1 ⇝* Term.obj l2) : Term.obj (Record.cons a not_in_a u_a l1) ⇝* Term.obj (Record.cons a not_in_a u_a l2)

Equations

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

def congOBJClos {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')))

Congruence for ⇝* in OBJ [KS22, Lemma A.4 (1)]

Equations

• congOBJClos ReflTransGen.refl isAttached = ⋯ ▸ ReflTransGen.refl
• congOBJClos (ReflTransGen.head red redMany) isAttached = ReflTransGen.head (Reduce.congOBJ b l red isAttached) (⋯ ▸ congOBJClos redMany (Insert.insert_new_isAttached isAttached))

def congDotClos {t t' : Term} {a : Attr} : (t ⇝* t') → (t.dot a ⇝* t'.dot a)

Congruence for ⇝* in DOT [KS22, Lemma A.4 (2)]

Equations

• congDotClos ReflTransGen.refl = ReflTransGen.refl
• congDotClos (ReflTransGen.head red redMany) = ReflTransGen.head (Reduce.congDOT t b a red) (congDotClos redMany)

def congAPPₗClos {t t' u : Term} {a : Attr} : (t ⇝* t') → (t.app a u ⇝* t'.app a u)

Congruence for ⇝* in APPₗ [KS22, Lemma A.4 (3)]

Equations

• congAPPₗClos ReflTransGen.refl = ReflTransGen.refl
• congAPPₗClos (ReflTransGen.head red redMany) = ReflTransGen.head (Reduce.congAPPₗ t b u a red) (congAPPₗClos redMany)

def congAPPᵣClos {t u u' : Term} {a : Attr} : (u ⇝* u') → (t.app a u ⇝* t.app a u')

Congruence for ⇝* in APPᵣ [KS22, Lemma A.4 (4)]

Equations

• congAPPᵣClos ReflTransGen.refl = ReflTransGen.refl
• congAPPᵣClos (ReflTransGen.head red redMany) = ReflTransGen.head (Reduce.congAPPᵣ t u b a red) (congAPPᵣClos redMany)

def par_to_redMany {t t' : Term} : (t ⇛ t') → (t ⇝* t')

Equivalence of ⇛ and ⇝ [KS22, Proposition 3.4 (3)]

Equations

• One or more equations did not get rendered due to their size.
• par_to_redMany (PReduce.pcongOBJ l l' premise) = par_to_redMany.fold_premise premise
• par_to_redMany (PReduce.pcong_ρ n) = ReflTransGen.refl
• par_to_redMany (PReduce.pcongDOT t_2 t'_2 a prtt') = congDotClos (par_to_redMany prtt')
• par_to_redMany (PReduce.pcongAPP t_2 t'_2 u u' a prtt' pruu') = red_trans (congAPPₗClos (par_to_redMany prtt')) (congAPPᵣClos (par_to_redMany pruu'))
• par_to_redMany (PReduce.pdot_c t_c c l preduce eq lookup_eq) = red_trans (congDotClos (par_to_redMany preduce)) (ReflTransGen.head (Reduce.dot_c t_c c l eq lookup_eq) ReflTransGen.refl)
• par_to_redMany (PReduce.pdot_cφ c l preduce eq lookup_eq isAttr) = red_trans (congDotClos (par_to_redMany preduce)) (ReflTransGen.head (Reduce.dot_cφ c l eq lookup_eq isAttr) ReflTransGen.refl)

def par_to_redMany.fold_premise {lst : List Attr} {al al' : Bindings lst} (premise : Premise al al') : Term.obj al ⇝* Term.obj al'

Equations

• One or more equations did not get rendered due to their size.
• par_to_redMany.fold_premise premise_3 = ReflTransGen.refl
• par_to_redMany.fold_premise (Premise.consVoid a premiseTail) = consBindingsRedMany a none (par_to_redMany.fold_premise premiseTail)

def parMany_to_redMany {t t' : Term} : (t ⇛* t') → (t ⇝* t')

Equivalence of ⇛ and ⇝ [KS22, Proposition 3.4 (4)]

Equations

• parMany_to_redMany ReflTransGen.refl = ReflTransGen.refl
• parMany_to_redMany (ReflTransGen.head red reds) = red_trans (par_to_redMany red) (parMany_to_redMany reds)

def redMany_to_parMany {t t' : Term} : (t ⇝* t') → (t ⇛* t')

Equivalence of ⇛ and ⇝ [KS22, Proposition 3.4 (2)]

Equations

• redMany_to_parMany ReflTransGen.refl = ReflTransGen.refl
• redMany_to_parMany (ReflTransGen.head red redMany) = ReflTransGen.head (reg_to_par red) (redMany_to_parMany redMany)

Confluence of ⇝

def weakEquivRegPar : WeakEquivalence PReduce Reduce

Equations

• weakEquivRegPar = (fun {a b : Term} => parMany_to_redMany, fun {a b : Term} => redMany_to_parMany)

def confluence_reduce : Confluence Reduce

Equations

• confluence_reduce = weak_equiv_keeps_confluence weakEquivRegPar confluence_preduce