data LogicFormula = A|B|C|D|E|F|G|H|I|J|K|L|M|N| 
       LogicFormula :&: LogicFormula | 
       LogicFormula :+: LogicFormula | 
       LogicFormula :-> LogicFormula |     
       Neg LogicFormula deriving (Eq,Read,Show)
data Sekv = [LogicFormula] :- [LogicFormula] deriving (Eq,Read,Show)
 
aks :: Sekv -> Bool
aks ([x] :- [y]) = if x == y then True else False
ax w = if (aks w) then w else error "w is not an axiom!"
 
p1  (g :- [x]) (g2 :- [y]) | g==g2     = g :- [x :&: y] 
                           | otherwise = error "g != g2"
p2  (g :- [x :&: y]) = g :- [x] 
p3  (g :- [x :&: y]) = g :- [y]
p4  (g :- [x]) y = g :- [x :+: y] 
p5  (g :- [y]) x = g :- [x :+: y] 
p6  ((z1:g1) :- [y1]) 
    ((x2:g2) :- [y2]) 
    (g3 :- [z3:+:x3]) | g1==g3 && g1==g3 && 
                        y1==y2 && z1==z3 && x2==x3 = g1 :- [y1] 
                      | otherwise = error "with ="
p7  ((x:g) :- [y]) = g :- [(x:->y)]
p8  (g  :- [x]) (g2 :- [x2:->y]) | g==g2 && x==x2 = g :- [y]
                                 | otherwise = error "g!=g2 or x!=x2"
p9  (((Neg x):g) :- []) = g :- [x]                              
p10 (g :- [x]) (g2 :- [x2]) | g==g2 && x==x2 = g :- []
                            | otherwise = error "g!=g2 or x!=x2"
p11 (g :- x) n = Tr_inList g n where
   Tr_inList gs n = x1s ++ (b:a:x2s) where
    (x1s,(a:b:x2s)) = splitAt (n-1) gs
 
p12 (g :- x) y = (y:g) :- x