### changeset 208:64ef1db53c49

...
author Shinji KONO Thu, 01 Aug 2019 08:28:20 +0900 3e4eb4da1453 e59e682ad120 OD.agda zf.agda 2 files changed, 10 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Thu Aug 01 00:13:07 2019 +0900
+++ b/OD.agda	Thu Aug 01 08:28:20 2019 +0900
@@ -567,18 +567,18 @@
choice-func' X ∋-p not = have_to_find
where
ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
-            ψ ox = ( x : Ordinal {suc n}) → x o< ox  → ¬ (def X x ) ∨ choiced X
+            ψ ox = ( x : Ordinal {suc n}) → x o< ox  → ( ¬ def X x ) ∨ choiced X
lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
lemma-ord  ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where
caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) ))
-               caseΦ lx prev | yes p = ? -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
-               caseΦ lx prev | no ¬p = ?
+               caseΦ lx prev | yes p = {!!} -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
+               caseΦ lx prev | no ¬p = {!!}
caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
-               caseOSuc lx x prev | yes p = ? -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
-               caseOSuc lx x prev | no ¬p =  ?
+               caseOSuc lx x prev | yes p = {!!} -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
+               caseOSuc lx x prev | no ¬p =  {!!}
have_to_find : choiced X
have_to_find with lemma-ord (od→ord X )
-            have_to_find | t = ?
+            have_to_find | t = dont-or ( t (od→ord X) {!!} ) {!!}
```
```--- a/zf.agda	Thu Aug 01 00:13:07 2019 +0900
+++ b/zf.agda	Thu Aug 01 08:28:20 2019 +0900
@@ -37,6 +37,10 @@
de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))

+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
-- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
-- mid-ex-neg {n} {A} = {!!}
```