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