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

comparison BAlgbra.agda @ 276:6f10c47e4e7a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate choice fix sup-o
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 09:02:52 +0900
parents 985a1af11bce
children d9d3654baee1
comparison
equal deleted inserted replaced
275:455792eaa611 276:6f10c47e4e7a
3 module BAlgbra {n : Level } (O : Ordinals {n}) where 3 module BAlgbra {n : Level } (O : Ordinals {n}) where
4 4
5 open import zf 5 open import zf
6 open import logic 6 open import logic
7 import OD 7 import OD
8 import ODC
8 9
9 open import Relation.Nullary 10 open import Relation.Nullary
10 open import Relation.Binary 11 open import Relation.Binary
11 open import Data.Empty 12 open import Data.Empty
12 open import Relation.Binary 13 open import Relation.Binary
38 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) 39 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) )
39 lemma4 {y} z with proj1 z 40 lemma4 {y} z with proj1 z
40 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) 41 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
41 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) 42 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
42 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x 43 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
43 lemma3 not = double-neg-eilm (FExists _ lemma4 not) -- choice 44 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice
44 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x 45 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
45 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A 46 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
46 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) 47 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
47 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B 48 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
48 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) 49 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))