-- This is a source code template for Curry programs.
main = prove $ Home Kat


data Person
  = Anna
  | Kat

data Proposition
  = PFalse
  | PTrue
  | And Proposition Proposition
  | Impl Proposition Proposition
  | NImpl Proposition Proposition
  | Home Person
  | Guilty Person

(/\) :: Proposition -> Proposition -> Proposition
p /\ q = And p q

(<---) :: Proposition -> Proposition -> Proposition
p <--- q = Impl p q

(<-/-) :: Proposition -> Proposition -> Proposition
p <-/- q = NImpl p q

(<-/->) :: Proposition -> Proposition -> Proposition
p <-/-> q = (p <-/- q) /\ (q <-/- p)

Not :: Proposition -> Proposition
Not p = PFalse <--- p

prove :: Proposition -> Success
prove p = axiom p
prove p = prove (p /\ q) where q free
prove p = prove (q /\ p) where q free
prove p = prove (p <--- q) & prove q where q free
prove (Not p) = prove (p <--- q) & prove (Not q) where q free
prove (Not p) = prove (p <-/- q) & prove q where q free
prove (Not q) = prove (p <-/- q) & prove p where p free

axiom :: Proposition -> Success
--axioms = Not (Home Anna)
axiom (Home Kat) = success
--axioms = Guilty Anna <-/-> Guilty Kat
--axioms = Guilty Anna <--- Not (Guilty Kat)
--axioms = Guilty Kat <--- Not (Guilty Anna)
--axioms = Guilty x <-/- Not (Home x) where x free
--axioms = Guilty x <--- Home x where x free