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

changeset 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
files HOD.agda
diffstat 1 files changed, 11 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Tue Jul 09 17:46:45 2019 +0900
+++ b/HOD.agda	Wed Jul 10 06:52:00 2019 +0900
@@ -318,6 +318,17 @@
          union-d X = record { def = λ y → def X (osuc y) }
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
+         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union (Ord x) ∋ z
+         ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z ))
+         ord-union→ x z u plt | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 plt))
+         ord-union→ x z u plt | tri< a ¬b ¬c | ()
+         ord-union→ x z u plt | tri≈ ¬a b ¬c  = subst ( λ k → k o< x ) b (proj1 plt)
+         ord-union→ x z u plt | tri> ¬a ¬b c = otrans (proj1 plt) c
+         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 )
+         ord-union← x z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
+             lemma : Ord x ∋ union-u {Ord x} {z} X∋z
+             lemma = def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl ?
+
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
          union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))