# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589069972 -32400
# Node ID a8f9c8a27e8d9889bb6513b62f64aed7a3876823
# Parent  2d77b6d12a2298e185642023075c14fa62c89e43
minimal from LEM

diff -r 2d77b6d12a22 -r a8f9c8a27e8d LEMC.agda
--- a/LEMC.agda	Sun May 10 00:18:59 2020 +0900
+++ b/LEMC.agda	Sun May 10 09:19:32 2020 +0900
@@ -32,6 +32,12 @@
 
 open choiced
 
+double-neg-eilm : {A : Set (suc n)} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-eilm  {A} notnot with p∨¬p A                         -- assuming axiom of choice
+... | case1 p = p
+... | case2 ¬p = ⊥-elim ( notnot ¬p )
+
+
 OD→ZFC : ZFC
 OD→ZFC   = record { 
     ZFSet = OD 
@@ -91,68 +97,45 @@
                min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
          open Minimal
          open _∧_
-         induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) →  (ne : ¬ (x == od∅ )) → Minimal x ne
-         induction {x} prev ne = c2
-            where
-             ch : choiced x
-             ch = choice-func x ne 
-             c1 : OD
-             c1 = a-choice ch   -- x ∋ c1
-             c2 : Minimal x ne
-             c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord  y)))  )
-             c2 | case1 Yes = record {
-                  min = c1
-               ;  x∋min = is-in ch 
-               ;  min-empty = Yes
-               }
-             c2 | case2 No = c3 where
-                y1 : OD
-                y1 =  record { def = λ y → ( def c1 y ∧ def x y) } 
-                noty1 : ¬ (y1 == od∅ )
-                noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) )
-                ch1 : choiced y1 --  a-choice ch1 ∈ c1 , a-choice ch1 ∈ x
-                ch1 = choice-func y1 noty1
-                c3 : Minimal x ne
-                c3 with is-o∅ (od→ord (a-choice ch1))
-                ... | yes eq =  record {
-                      min = od∅
-                   ;  x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) 
-                   ;  min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) )
-                  } 
-                ... | no n =  record {
-                      min = min min3
-                   ;  x∋min = x∋min3 (x∋min min3)
-                   ;  min-empty = min3-empty -- λ y p → min3-empty min3 y p    -- p : (min min3 ∋ y) ∧ (x ∋ y)
-                  }  where
-                       lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ 
-                       lemma eq = begin 
-                           od→ord (a-choice ch1) 
-                         ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩
-                           od→ord od∅  
-                         ≡⟨ ord-od∅ ⟩
-                           o∅
-                         ∎ where open ≡-Reasoning 
-                       --  Minimal (a-choice ch1) ch1not
-                       --      min ∈ a-choice ch1 ,  min ∩ a-choice ch1  ≡ ∅
-                       ch1not : ¬ (a-choice ch1 == od∅)
-                       ch1not ch1=0 = n (lemma ch1=0)
-                       min3 : Minimal (a-choice ch1) ch1not
-                       min3 =  prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))
-                       x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3
-                       x∋min3 lt = {!!}
-                       min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y))
-                       min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } --  (min min3 ∋ y) ∧ (a-choice ch1 ∋ y)
-                           -- p : (min min3 ∋ y) ∧ (x ∋ y)
-
-                   
-         Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne
-         Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) 
+         --
+         --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
+         --
+         induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅<  u∋x))
+              →  (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅<  u∋x)
+         induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
+         ... | case1 P =
+              record { min = x
+                ;     x∋min = u∋x
+                ;     min-empty = P
+              } 
+         ... | case2 NP = 
+              record { min = min min2
+                ;     x∋min = x∋min min2
+                ;     min-empty = min-empty min2
+             
+               } where
+              p : OD
+              p  = record { def = λ y1 → def x  y1 ∧ def u y1 }
+              np : ¬ (p == od∅)
+              np p∅ =  NP (λ y p∋y → ∅< p∋y p∅ ) 
+              y1choice : choiced p
+              y1choice = choice-func p np
+              y1 : OD
+              y1 = a-choice y1choice
+              y1prop : (x ∋ y1) ∧ (u ∋ y1)
+              y1prop = is-in y1choice
+              min2 : Minimal u (∅< (proj2 y1prop))
+              min2 = prev (proj1 y1prop) u (proj2 y1prop)
+         Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅<  u∋x)
+         Min2 x u u∋x = (ε-induction {λ y →  (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x) } induction x u u∋x ) 
+         cx : {x : OD} →  ¬ (x == od∅ ) → choiced x 
+         cx {x} nx = choice-func x nx
          minimal : (x : OD  ) → ¬ (x == od∅ ) → OD 
-         minimal x not = min (Min1 x not ) 
+         minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 
          x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min1 x ne) 
+         x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) 
          minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
-         minimal-1 x ne y = min-empty (Min1 x ne ) y
+         minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y