def complete_development : Term → Term

Complete Development [KS22, Definition 3.6]

Equations

• One or more equations did not get rendered due to their size.
• complete_development (Term.loc n) = Term.loc n
• complete_development (Term.obj bnds) = Term.obj (complete_developmentLst bnds)

def complete_developmentLst {lst : List Attr} : Bindings lst → Bindings lst

Equations

• complete_developmentLst Record.nil = Record.nil
• complete_developmentLst (Record.cons a lst_2 none tail) = Record.cons a lst_2 none (complete_developmentLst tail)
• complete_developmentLst (Record.cons a lst_2 (some t) tail) = Record.cons a lst_2 (some (complete_development t)) (complete_developmentLst tail)

def term_to_development (t : Term) : t ⇛ complete_development t

Term reduces (⇛) to its complete development [KS22, Proposition 3.7]

Equations

• One or more equations did not get rendered due to their size.
• term_to_development (Term.loc n) = id (prefl (Term.loc n))
• term_to_development (Term.obj bnds) = id (PReduce.pcongOBJ bnds (complete_developmentLst bnds) (term_to_development_Lst bnds))

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

Equations

• term_to_development_Lst Record.nil = id Premise.nil
• term_to_development_Lst (Record.cons a lst_2 none tail) = id (Premise.consVoid a (term_to_development_Lst tail))
• term_to_development_Lst (Record.cons a lst_2 (some t) tail) = id (Premise.consAttached a t (complete_development t) (term_to_development t) (term_to_development_Lst tail))

def half_diamond {t t' : Term} (preduce : t ⇛ t') : t' ⇛ complete_development t

Half Diamond [KS22, Proposition 3.8]

Equations

• One or more equations did not get rendered due to their size.
• half_diamond (PReduce.pcongOBJ l newAttrs premise) = id (PReduce.pcongOBJ newAttrs (complete_developmentLst l) (half_diamond.make_premise premise))
• half_diamond (PReduce.pcong_ρ n) = id (prefl (Term.loc n))

def half_diamond.make_premise {lst : List Attr} {l l' : Bindings lst} (premise : Premise l l') : Premise l' (complete_developmentLst l)

Equations

• One or more equations did not get rendered due to their size.
• half_diamond.make_premise premise_3 = id Premise.nil
• half_diamond.make_premise (Premise.consVoid a premise_tail) = id (Premise.consVoid a (half_diamond.make_premise premise_tail))

def takahashi_preduce : Takahashi PReduce

Equations

• takahashi_preduce = ⟨complete_development, fun {s u : Term} => half_diamond⟩

def diamond_preduce : DiamondProperty PReduce

Equations

• diamond_preduce = takahashi_implies_diamond takahashi_preduce

def confluence_preduce : Confluence PReduce

Equations

• confluence_preduce = diamond_implies_confluence diamond_preduce