propositional/model_theory/bool-zf.elf

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "bool.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../../set_theories/zfc/bool.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../meta/sttifol-zf.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Bool-ZF : Bool -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   %include STTIFOLEQ-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   bool' := cbool.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   0     := ⊥.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   1     := ⊤.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   cons  := ccons.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   boole := ctnd.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   ifte  := Lambda [c] Lambda [t] Lambda [e] ifte c t e.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   ifteT := [C][T][E] impI [p] trans beta3 (EqcongEr ([x] ifte x T E Eq T) p ifte1).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder   ifteE := [C][T][E] impI [p] trans beta3 (EqcongEr ([x] ifte x T E Eq E) p ifte0).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova}.