module Htaut.Theorem.Basic where
import Htaut.Proposition
import Htaut.Proving
import Htaut.Theorem.Elementary
syllogism :: (Prop p, Prop q, Prop r) =>
Prove ((p -> q) -> ((q -> r) -> (p -> r)))
syllogism = return (flip (.))
syllogism' :: (Prop p, Prop q, Prop r) =>
Prove ((q -> r) -> ((p -> q) -> (p -> r)))
syllogism' = return (.)
propagate :: (Prop p, Prop q) => Prove (p -> ((p -> q) -> q))
propagate = return (flip ($))
conditionSeperate :: (Prop p, Prop q, Prop r) =>
Prove ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
conditionSeperate = return (\pqr pq p -> pqr p (pq p))
conditionCommute :: (Prop p, Prop q, Prop r) =>
Prove ((p -> (q -> r)) -> (q -> (p -> r)))
conditionCommute = return flip
identity :: (Prop p) => Prove (p -> p)
identity = return id
conditionAdd :: (Prop p, Prop q) => Prove (q -> (p -> q))
conditionAdd = return const
dunsScotus :: (Prop p, Prop q) => Prove (Neg p -> (p -> q))
dunsScotus = return (bottomImply .)
dunsScotus' :: (Prop p, Prop q) => Prove (p -> (Neg p -> Neg q))
dunsScotus' = return (flip (bottomImply .))