Coqで実装したので停止性と型安全性が保証できているので構文的に完全な cnf 変換

cnf.v

Definition x := nat.
Inductive t:=X:x->t|True:t|False:t|N:t->t|A:t*t->t|O:t*t->t.
Inductive n:=NX:x->n|NTrue:n|NFalse:n|NN:x->n|NA:n*n->n|NO:n*n->n.
Fixpoint t2n(t0:t):n :=
  match t0 with
  | N(a) => t2nneg a
  | A(a,b) => NO(t2n a,t2n b)
  | O(a,b) => NA(t2n a,t2n b)
  | X x => NX x
  | True => NTrue
  | False => NFalse
  end
with t2nneg(t0:t) :n :=
  match t0 with
  | N(N(a)) => t2nneg a
  | N(A(a,b)) => NO(t2n a,t2n b)
  | N(O(a,b)) => NA(t2n a,t2n b)
  | N(x) => t2n x
  | True => NFalse
  | False => NTrue
  | A(a,b) => NO(t2nneg a,t2nneg b)
  | O(a,b) => NA(t2nneg a,t2nneg b)
  | X x => NN x
  end.
Inductive d:=DX:x->d|DTrue:d|DFalse:d|DN:x->d|DO:d*d->d.
Fixpoint dod(t0:d) (t1:d) :d :=
  match t0,t1 with
  | DTrue,t => DTrue
  | t,DTrue => DTrue
  | t,DFalse => t
  | DFalse,t => t
  | DX x,DX y => if Nat.eqb x y then DX x else DO(DX x,DX y)
  | DN x,DN y => if Nat.eqb x y then DN x else DO(DN x,DN y)
  | DX x,DN y => if Nat.eqb x y then DTrue else DO(DX x,DN y)
  | DN x,DX y => if Nat.eqb x y then DTrue else DO(DN x,DX y)
  | DO(a,b),y => dod a (dod b y)
  | x,y => DO(x,y)
  end.
Inductive c:=C:d->c|CA:d*c->c.
Fixpoint doc (d1:d) (c2:c): c :=
  match c2 with
  | C d2 => C (dod d1 d2)
  | CA(d2,c2) => CA(dod d1 d2,doc d1 c2)
  end.
Fixpoint dad (d1:d) (d2:d): c:= CA(d1,C d2).
Fixpoint dac (d1:d) (c2:c): c:= CA(d1,c2).
Fixpoint cac (c1:c) (c2:c): c:=
  match c1 with
  | C d1 => dac d1 c2
  | CA(d1,c1) => dac d1 (cac c1 c2)
  end.
Fixpoint coc (c1:c) (c2:c): c :=
  match c1 with
  | C d1 => doc d1 c2
  | CA(d1,c1) => cac (doc d1 c2) (coc c1 c2)
  end.
Fixpoint nac (n1 : n) (c2:c): c :=
  match n1 with
  | NX x => dac (DX x) c2
  | NN x => dac (DN x) c2
  | NTrue => dac DTrue c2
  | NFalse => dac DFalse c2
  | NA(a,b) => nac b (nac a c2)
  | NO(a,b) => cac (coc (nac b (C DTrue)) (nac a (C DTrue))) c2
  end.
Definition n2c (n:n): c := nac n (C DTrue).
Definition t2c (t:t): c := n2c (t2n t).