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

comparison HOD.agda @ 153:f1801c4735d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
union continue ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 10 Jul 2019 06:52:00 +0900
parents 996a67042f50
children e51c23eb3803
comparison
equal deleted inserted replaced
152:996a67042f50 153:f1801c4735d3
316 316
317 union-d : (X : OD {suc n}) → OD {suc n} 317 union-d : (X : OD {suc n}) → OD {suc n}
318 union-d X = record { def = λ y → def X (osuc y) } 318 union-d X = record { def = λ y → def X (osuc y) }
319 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} 319 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
320 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 320 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
321 ord-union→ : (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union (Ord x) ∋ z
322 ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z ))
323 ord-union→ x z u plt | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 plt))
324 ord-union→ x z u plt | tri< a ¬b ¬c | ()
325 ord-union→ x z u plt | tri≈ ¬a b ¬c = subst ( λ k → k o< x ) b (proj1 plt)
326 ord-union→ x z u plt | tri> ¬a ¬b c = otrans (proj1 plt) c
327 ord-union← : (x : Ordinal) (z : OD) (X∋z : Union (Ord x) ∋ z) → (Ord x ∋ union-u {Ord x} {z} X∋z ) ∧ (union-u {Ord x} {z} X∋z ∋ z )
328 ord-union← x z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
329 lemma : Ord x ∋ union-u {Ord x} {z} X∋z
330 lemma = def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl ?
331
321 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 332 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
322 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) 333 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
323 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) 334 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
324 union→ X z u xx | tri< a ¬b ¬c | () 335 union→ X z u xx | tri< a ¬b ¬c | ()
325 union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b 336 union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b