module GentzenEgs where
import Text.PrettyPrint.HughesPJ
import Prop
import Tactics
import Examples
import L

ex1 = replay (SequentM [a,ImpliesP a b] [b]) [impliesL 2, weakening 2, axiom 1 1, axiom 2 1]
ex2 = replay (SequentM []               [aimpliesbimpliesa]) [impliesR 1, impliesR 1, axiom 2 1]
ex3 = replay (SequentM []               [ImpliesP a a]) [impliesR 1,axiom 1 1]
ex4 = replay (SequentM [OrP a b]        [OrP b a]) [orR 1,orL 1,weakening 1, axiom 1 1,weakening 2,axiom 1 1]
ex5 = replay (SequentM [OrP a b]        [OrP b a]) [orR 1,orL 1,axiom 1 2, axiom 1 1]
ex6 = replay (SequentM []               [impliesDistributes]) [iR, iR, iR, iL, ax, iL, ax, iL, ax, ax]
ex7 = replay (SequentM []               [pierce]) [iR, iL, iR, ax, ax]
ex8 = replay (SequentM []               [a,NotP a]) [nR,ax]

tests = sep [ex1,ex2,ex3,ex4,ex5,ex6,ex7,ex8]

goal = SequentM [] [impliesDistributes]