Mercurial > hg > Members > kono > Proof > ZF-in-agda

annotate BAlgbra.agda @ 369:17adeeee0c2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Select and Replace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 19 Jul 2020 10:02:43 +0900
parents 2a8a51375e49
children 6c72bee25653
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
369
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
1 {-# OPTIONS --allow-unsolved-metas #-}
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Ordinals
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module BAlgbra {n : Level } (O : Ordinals {n}) where
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import zf
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import logic
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 import OD
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
9 import ODC
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Nullary
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Data.Empty
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Relation.Binary
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Relation.Binary.Core
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Relation.Binary.PropositionalEquality
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open inOrdinal O
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open OD O
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 open OD.OD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
22 open ODAxiom odAxiom
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
23 open HOD
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 open _∧_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 open _∨_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 open Bool
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
360
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
29 --_∩_ : ( A B : HOD ) → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
30 --A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
31 -- odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
33 _∪_ : ( A B : HOD ) → HOD
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
34 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
35 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
36 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
37 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
38 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
40 _＼_ : ( A B : HOD ) → HOD
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
41 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
43 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
45 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 lemma1 {x} lt = lemma3 lt where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
47 lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 lemma4 {y} z with proj1 z
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
49 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) )
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
50 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) )
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
51 lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
52 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
53 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
54 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
55 (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x}))
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
56 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
57 (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
369
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
59 ∩-Select : { A B : HOD } → Select A ( λ x _ → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
369
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
61 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
62 lemma1 {x} lt = record { proj1 = proj1 {!!} ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 {!!} )) }
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
63 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
64 lemma2 {x} lt = {!!} -- record { proj1 = proj1 lt ; proj2 =
17adeeee0c2a fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 360
diff changeset
65 -- record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
67 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
69 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 lemma1 {x} lt with proj2 lt
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
73 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) }
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) }
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
77 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
79 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
82 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 lemma2 {x} lt with proj1 lt | proj2 lt
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 lemma2 {x} lt | case1 cp | _ = case1 cp
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 lemma2 {x} lt | _ | case1 cp = case1 cp
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 record IsBooleanAlgebra ( L : Set n)
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 ( b1 : L )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 ( b0 : L )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ( -_ : L → L )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 ( _+_ : L → L → L )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ( _*_ : L → L → L ) : Set (suc n) where
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 field
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 +-sym : {a b : L } → a + b ≡ b + a
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 -sym : {a b : L } → a * b ≡ b * a
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 -aab : {a b : L } → a + ( a * b ) ≡ a
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 *-aab : {a b : L } → a * ( a + b ) ≡ a
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 a+0 : {a : L } → a + b0 ≡ a
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 a*1 : {a : L } → a * b1 ≡ a
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 a+-a1 : {a : L } → a + ( - a ) ≡ b1
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 a*-a0 : {a : L } → a * ( - a ) ≡ b0
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 record BooleanAlgebra ( L : Set n) : Set (suc n) where
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 field
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 b1 : L
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 b0 : L
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 -_ : L → L
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 _++_ : L → L → L
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 _**_ : L → L → L
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116