構文的に完全なnnf変換

nnf.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|NNX:x->n|NA:n*n->n|NO:n*n->n.
Fixpoint nnf(t0:t):n :=
  match t0 with
  | N(a) => neg a
  | A(a,b) => NO(nnf a,nnf b)
  | O(a,b) => NA(nnf a,nnf b)
  | X x => NX x
  | True => NTrue
  | False => NFalse
  end
with neg(t0:t) :n :=
  match t0 with
  | N(N(a)) => neg a
  | N(A(a,b)) => NO(nnf a,nnf b)
  | N(O(a,b)) => NA(nnf a,nnf b)
  | N(x) => nnf x
  | True => NFalse
  | False => NTrue
  | A(a,b) => NO(neg a,neg b)
  | O(a,b) => NA(neg a,neg b)
  | X x => NNX x
  end.