%read "modules.elf".

%read "base-zf.elf".

%view TruthMOD-ZF : TruthMOD -> Boolean = {

%include BasePLMOD-ZF.

true' := ⊤.

true1 := refl.

}.

%view FalsityMOD-ZF : FalsityMOD -> Boolean = {

%include BasePLMOD-ZF.

false' := ⊥.

false0 := refl.

}.

%view NEGMOD-ZF : NEGMOD -> Boolean = {

%include BasePLMOD-ZF.

not' := lambda [a] ¬ a.

not1 := [A:ℬ] impI [p: ded A Eq ⊥] trans beta (EqcongEr ([a] ¬ a Eq ⊤) p ∖neut).

not0 := [A:ℬ] impI [p: ded A Eq ⊤] trans beta (EqcongEr ([a] ¬ a Eq ⊥) p ∖rep).

}.

%view IMPMOD-ZF : IMPMOD -> Boolean = {

%include BasePLMOD-ZF.

imp' := Lambda [a] Lambda [b] a → b.

imp1 := [A][B] impI [p] trans beta2 (EqcongEr ([x] ⊤ ∖ x Eq ⊤)

(orE p ([q: ded A Eq ⊥] EqcongEr ([a] a ∖ B Eq ⊥) q ∖attr)

([q: ded B Eq ⊤] EqcongEr ([b] A ∖ b Eq ⊥) q ∖rep )

) ∖neut).

imp0 := [A][B] impI [p] trans beta2 (EqcongEr ([x] ⊤ ∖ x Eq ⊥)

(trans (EqcongEr ([x] A ∖ x Eq A) (andEr p) ∖neut) (andEl p))

∖rep).

}.

%view CONJMOD-ZF : CONJMOD -> Boolean = {

%include BasePLMOD-ZF.

and' := Lambda [a] Lambda [b] a ∧ b.

and1 := [A][B] impI [p : ded A Eq ⊤ and B Eq ⊤] trans beta2

(EqcongEr ([x:ℬ] A ∧ x Eq ⊤)

(andEr p)

(EqcongEr ([x:ℬ] x ∧ ⊤ Eq ⊤) (andEl p) ∩idem)

).

and0 := [A][B] impI [p : ded A Eq ⊥ or B Eq ⊥] trans beta2

(orE p

([pl : ded A Eq ⊥] EqcongEr ([x:ℬ] x ∧ B Eq ⊥) pl (EqcongEl ([x:ℬ] x Eq ⊥) ∩comm ∩attr))

([pr : ded B Eq ⊥] EqcongEr ([x:ℬ] A ∧ x Eq ⊥) pr ∩attr)

).

}.

%view DISJMOD-ZF : DISJMOD -> Boolean = {

%include BasePLMOD-ZF.

or' := Lambda [a] Lambda [b] a ∨ b.

or1 := [A][B] impI [p : ded A Eq ⊤ or B Eq ⊤] trans beta2

(orE p

([pl : ded A Eq ⊤] EqcongEr ([x:ℬ] x ∨ B Eq ⊤) pl (EqcongEl ([x:ℬ] x Eq ⊤) ∪comm ∪attr))

([pr : ded B Eq ⊤] EqcongEr ([x:ℬ] A ∨ x Eq ⊤) pr ∪attr)

).

or0 := [A][B] impI [p : ded A Eq ⊥ and B Eq ⊥] trans beta2

(EqcongEr ([x:ℬ] A ∨ x Eq ⊥)

(andEr p)

(EqcongEr ([x:ℬ] x ∨ ⊥ Eq ⊥) (andEl p) ∪idem)).

}.