fact: Fixpoint unit_nf (t : term) : term := match t with | Var _ => t | Term f nil => Term f nil | Term f (t1 :: nil) => Term f ((unit_nf t1) :: nil) | Term f (t1 :: t2 :: nil) => match unit_theory f with | LU u => let ut1 := unit_nf t1 in if T.eq_bool ut1 (Term u nil) then unit_nf t2 else Term f (ut1 :: (unit_nf t2) :: nil) | RU u => let ut2 := unit_nf t2 in if T.eq_bool ut2 (Term u nil) then unit_nf t1 else Term f ((unit_nf t1) :: ut2 :: nil) | U u => let ut1 := unit_nf t1 in let ut2 := unit_nf t2 in if T.eq_bool ut1 (Term u nil) then ut2 else if T.eq_bool ut2 (Term u nil) then ut1 else Term f (ut1 :: ut2 :: nil) | Nothing => Term f ((unit_nf t1) :: (unit_nf t2) :: nil) end | Term f l => Term f (map unit_nf l) end.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)