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

changeset 201:a1a7caa8b305

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jul 2019 01:12:24 +0900
parents 57be355d1336
children ed88384b5102
files OD.agda
diffstat 1 files changed, 9 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jul 29 23:50:00 2019 +0900
+++ b/OD.agda	Tue Jul 30 01:12:24 2019 +0900
@@ -568,9 +568,15 @@
             <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
             <-not {X} ox =  ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) 
             ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X
-            ind {y} ψ nox with ∋-p X y
-            ind {y} ψ nox | yes p = record { a-choice = y ; is-in = p }
-            ind {y} ψ nox | no ¬p = {!!}
+            ind {x} ψ nox = lemma (od→ord x) nox where
+                 lemma : (ox : Ordinal {suc n}) → <-not {X} ox → choiced X
+                 lemma ox nox with ∋-p X (ord→od ox)
+                 ... | yes p = record { a-choice = ord→od ox ; is-in = p }
+                 lemma record { lv = Zero ; ord = (Φ 0) } nox | no ¬p = {!!}
+                 lemma record { lv = lx ; ord = (OSuc lx ox) } nox | no ¬p = lemma record { lv = lx ; ord = ox } {!!}
+                 lemma record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } nox | no ¬p = lemma  record { lv = lx ; ord = Φ lx } lemma2 where
+                      lemma2 : ( y : Ordinal {suc n}) → record { lv = lx ; ord = Φ lx } o< osuc y → ¬ (X ∋ (ord→od y))
+                      lemma2 y lt = {!!}
             lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X
             lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x)
             lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y)