c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder bool : type = elem bool'.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder cons : ded not (1 eq 0).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder boole : {A} ded (A eq 1 or A eq 0).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ifte : elem (bool' → bool' → bool' → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ifteT : ded C eq 1 imp (ifte @ C @ T @ E) eq T.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ifteE : ded C eq 0 imp (ifte @ C @ T @ E) eq E.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ¬ : bool -> bool = [a] ifte @ a @ 0 @ 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ∧ : bool -> bool -> bool = [a][b] ifte @ a @ b @ 0. %infix left 10 ∧.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ∨ : bool -> bool -> bool = [a][b] ifte @ a @ 1 @ b. %infix left 10 ∨.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ⇒ : bool -> bool -> bool = [a][b] ifte @ a @ b @ 1. %infix none 10 ⇒.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not1 : ded A eq 0 -> ded (¬ A) eq 1 = [p] impE ifteE p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not0 : ded A eq 1 -> ded (¬ A) eq 0 = [p] impE ifteT p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp1 : ded A eq 0 or B eq 1 -> ded (A ⇒ B) eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] orE p ([q] impE ifteE q) ([q] orE (boole A) ([r: ded A eq 1] trans (impE ifteT r) q)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([r: ded A eq 0] impE ifteE r)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp0 : ded A eq 1 and B eq 0 -> ded (A ⇒ B) eq 0 = [p] trans (impE ifteT (andEl p)) (andEr p).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and1 : ded A eq 1 and B eq 1 -> ded (A ∧ B) eq 1 = [p] trans (impE ifteT (andEl p)) (andEr p).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and0 : ded A eq 0 or B eq 0 -> ded (A ∧ B) eq 0
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] orE p ([q] impE ifteE q) ([q] orE (boole A) ([r: ded A eq 1] trans (impE ifteT r) q)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([r: ded A eq 0] impE ifteE r)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or1 : ded A eq 1 or B eq 1 -> ded (A ∨ B) eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] orE p ([q] impE ifteT q) ([q] orE (boole A) ([r: ded A eq 1] impE ifteT r)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([r: ded A eq 0] trans (impE ifteE r) q)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or0 : ded A eq 0 and B eq 0 -> ded (A ∨ B) eq 0 = [p] trans (impE ifteE (andEl p)) (andEr p).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder contra : ded A eq 0 -> ded A eq 1 -> ded false
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p][q] (notE' (trans (sym q) p) cons).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder indirect : (ded A eq 0 -> ded false) -> ded A eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [f] orE (boole A)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([p : ded A eq 1] p)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([p : ded A eq 0] falseE (f p) (A eq 1)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder indirect' : (ded A eq 1 -> ded false) -> ded A eq 0
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [f] orE (boole A)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([p : ded A eq 1] falseE (f p) (A eq 0))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([p : ded A eq 0] p).