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

changeset 107:745bee73b444

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add assumption
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Jun 2019 19:55:37 +0900
parents c31ac67e9ecb
children f91e425b341d
files ordinal-definable.agda
diffstat 1 files changed, 14 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Sun Jun 16 12:26:18 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 16 19:55:37 2019 +0900
@@ -164,7 +164,7 @@
    c3 lx (OSuc .lx x₁) d not | t | ()
 
 transitive-Ord : {n : Level } { z y x : Ordinal {suc n} } → Ord z ∋ Ord y → Ord y ∋ Ord x → Ord z  ∋ Ord x
-transitive-Ord = {!!}
+transitive-Ord {n} {z} {y} {x} z∋y x∋y  =  o<→c< ( ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y )  )
 
 
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
@@ -229,8 +229,14 @@
 
 open _∧_
 
-ord-od∅ :  {n : Level} → o∅ {n} ≡ od→ord (Ord (o∅ {n}))
-ord-od∅ = ==→o≡  {!!}
+ord-od∅ :  {n : Level} → o∅ {suc n} ≡ od→ord (Ord (o∅ {suc n}))
+ord-od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (Ord (o∅ {suc n})))
+ord-od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
+    lemma :  o∅ {suc n } o< (od→ord (Ord (o∅ {suc n}))) → ⊥
+    lemma lt with  o<→c< lt
+    lemma lt | t = o<¬≡ _ _ refl t
+ord-od∅ {n} | tri≈ ¬a b ¬c = b
+ord-od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 
 
 ¬∅=→∅∈ :  {n : Level} →  { x : Ordinal {suc n} } → ¬ (  Ord x  == od∅ {suc n} ) → Ord x ∋ od∅ {suc n} 
@@ -238,6 +244,7 @@
 ¬∅=→∅∈ {n} {x} ne | yes refl = ⊥-elim ( ne (eq-sym (eq-refl) ))
 ¬∅=→∅∈ {n} {x} ne | no ¬p = o<-subst (∅5 ¬p) ord-od∅ refl
 
+
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
@@ -328,12 +335,13 @@
          empty x (case2 ())
 
          power→Ord : (A t : Ordinal) → Power (Ord A) ∋ (Ord t) → {x : OD} → Ord t ∋ x → Ord A ∋ x
-         power→Ord A t P∋t {x} t∋x = {!!} where
+         power→Ord A t P∋t {x} t∋x = proj1 lemma-s where
               minsup :  OD
               minsup =  ZFSubset (Ord A) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord A) (ord→od x))))) 
               lemma-t : csuc minsup ∋ Ord t
-              lemma-t with  sup-lb {!!}
-              ... | c = {!!}
+              lemma-t = ? -- o<→c< (sup-lb  P∋t)
+              lemma-s : ZFSubset (Ord A) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord A) (ord→od x)))))  ∋ x
+              lemma-s = {!!}
          power←Ord : (A t : Ordinal) → ({x : OD} → (Ord t ∋ x → Ord A ∋ x)) → Power (Ord A) ∋ Ord t
          power←Ord = {!!}
          ---