type Expression =
                | Expr of bool
                | Negation of Expression
                | Disjunction of Expression * Expression
                | Conjunction of Expression * Expression
                | Implication of Expression * Expression
                | Bimplication of Expression * Expression

let rec nnf expr = match expr with
                | (Expr expr) -> (Expr expr)
                | (Negation (Negation (expr))) -> (nnf expr)
                | (Conjunction (expr1, expr2)) -> (Conjunction ((nnf expr1), (nnf expr2)))
                | (Disjunction (expr1, expr2)) -> (Disjunction ((nnf expr1), (nnf expr2)))
                | (Negation (Conjunction (expr1, expr2))) -> (Disjunction ((nnf (Negation expr1)), (nnf (Negation expr2))))
                | (Negation (Disjunction (expr1, expr2))) -> (Conjunction ((nnf (Negation expr1)), (nnf (Negation expr2))))
                | (Negation (Bimplication (expr1, expr2))) -> nnf (Negation (Conjunction ((Implication (expr1, expr2)), (Implication (expr2, expr1)))))
                | (Negation (Implication (expr1, expr2))) -> nnf (Conjunction (expr1, (Negation expr2)))
                | (Negation expr) -> (Negation expr)
                | (Implication (expr1, expr2)) -> nnf (Negation (Conjunction (expr1, (Negation expr2))))
                | (Bimplication (expr1, expr2)) -> nnf (Conjunction ((Implication (expr1, expr2)), (Implication (expr2, expr1))))