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

changeset 192:38ecc75d93ce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jul 2019 14:50:56 +0900
parents 9eb6a8691f02
children 0b9645a65542
files OD.agda
diffstat 1 files changed, 6 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Sun Jul 28 14:07:08 2019 +0900
+++ b/OD.agda	Sun Jul 28 14:50:56 2019 +0900
@@ -501,14 +501,12 @@
          choice X {A} X∋A not = x∋minimul A not
 
          choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
-         choice-func' X ∋-p not = lemma (lv (od→ord X )) (ord (od→ord X)) where
-             lemma : (lx : Nat ) ( ox : OrdinalD lx )  → OD {suc n}
-             lemma lx ox  with ∋-p X (ord→od record { lv = lx ; ord = ox })
-             lemma lx ox | yes p = (ord→od record { lv = lx ; ord = ox })
-             lemma Zero (Φ 0)  | no ¬p = od∅
-             lemma Zero (OSuc 0 ox)  | no ¬p = lemma  Zero ox 
-             lemma (Suc lx) (Φ (Suc lx))  | no ¬p = {!!}
-             lemma (Suc lx) (OSuc (Suc lx) ox)  | no ¬p = lemma ( Suc lx ) ox 
+         choice-func' X ∋-p not = lemma o∅  {!!} {!!} where
+             lemma : (ox : Ordinal {suc n} ) → ( ox o< osuc (od→ord X) ) → ((oy : Ordinal ) → oy o< ox → ¬ ( X ∋ ord→od oy ) )  → OD {suc n}
+             lemma ox lt l∅ with ∋-p X (ord→od ox)
+             lemma ox lt l∅ | yes p = ord→od ox
+             lemma ox (case1 x) l∅ | no ¬p = lemma (record { lv = Suc (lv ox); ord = Φ (Suc (lv ox))}) (case1 {!!}) {!!}
+             lemma ox (case2 x) l∅ | no ¬p = lemma (record { lv = lv ox; ord = OSuc (lv ox) (ord ox)}) {!!} {!!}
 
          --
          -- another form of regularity