# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564622536 -32400
# Node ID e59e682ad120a58eb064ee033c69f92c44606668
# Parent  64ef1db53c499e8d4644914b9a83e8521ef25eb1
∀-imply-or

diff -r 64ef1db53c49 -r e59e682ad120 OD.agda
--- a/OD.agda	Thu Aug 01 08:28:20 2019 +0900
+++ b/OD.agda	Thu Aug 01 10:22:16 2019 +0900
@@ -563,22 +563,52 @@
             field
                 a-choice : OD {suc n}
                 is-in : X ∋ a-choice
-         choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → choiced X
-         choice-func' X ∋-p not = have_to_find 
+         choice-func' : (X : OD {suc n} ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
+         choice-func' X p∨¬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
+               ∋-p' : (A x : OD {suc n} ) → Dec ( A ∋ x ) 
+               ∋-p' A x with p∨¬p ( A ∋ x )
+               ∋-p' A x | case1 t = yes t
+               ∋-p' A x | case2 t = no t
+               ∀-imply-or :  {n : Level}  {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
+                   → ((x : Ordinal {suc n}) → A x ∨ B) →  ((x : Ordinal {suc n}) → A x) ∨ B
+               ∀-imply-or {n} {A} {B} ∀AB with p∨¬p  ((x : Ordinal {suc n}) → A x)
+               ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
+               ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
+                    lemma : ¬ ((x : Ordinal {suc n}) → A x) →  B
+                    lemma not with p∨¬p B
+                    lemma not | case1 b = b
+                    lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
                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 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 = lemma where
+                    lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
+                    lemma1 x with trio< x (ordinal lx (Φ lx))
+                    lemma1 x | tri< a ¬b ¬c with prev x a
+                    lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 {!!}
+                    lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
+                    lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
+                    lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
+                    lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
+                    lemma = ∀-imply-or lemma1
                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 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 (case1 not_found) | no ¬p = case1 lemma where
+                    lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
+                    lemma y lt with trio< y (ordinal lx x )
+                    lemma y lt | tri< a ¬b ¬c = not_found y a
+                    lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
+                    lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
+                    lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
+                    lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
+               caseOSuc lx x (case2 found) | no ¬p = case2 found
             have_to_find : choiced X
             have_to_find with lemma-ord (od→ord X )
-            have_to_find | t = dont-or ( t (od→ord X) {!!} ) {!!}
+            have_to_find | t = dont-or  t  {!!}
 
diff -r 64ef1db53c49 -r e59e682ad120 zf.agda
--- a/zf.agda	Thu Aug 01 08:28:20 2019 +0900
+++ b/zf.agda	Thu Aug 01 10:22:16 2019 +0900
@@ -41,6 +41,10 @@
 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
 dont-or {A} {B} (case2 b) ¬A = b
 
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
 -- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
 -- mid-ex-neg {n} {A} = {!!}