### changeset 280:a2991ce14ced

...
author Shinji KONO Sat, 09 May 2020 17:35:56 +0900 197e0b3d39dc 81d639ee9bfd LEMC.agda 1 files changed, 23 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
```--- a/LEMC.agda	Sat May 09 16:41:40 2020 +0900
+++ b/LEMC.agda	Sat May 09 17:35:56 2020 +0900
@@ -84,16 +84,32 @@
eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt)
; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
}
-         minimal-choice : (X : OD ) → ¬ (X == od∅) → choiced X
-         minimal-choice X ne = choice-func {!!} ne
+         record Minimal (x : OD)  : Set (suc n) where
+           field
+               min : OD
+               x∋min :  ¬ (x == od∅ ) → x ∋ min
+               min-empty :  ¬ (x == od∅ ) → (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+         open Minimal
+         induction : {x : OD} → ({y : OD} → x ∋ y → Minimal y) → Minimal x
+         induction {x} prev = record {
+                  min = {!!}
+               ;  x∋min = {!!}
+               ;  min-empty = {!!}
+            } where
+             c1 : OD
+             c1 = a-choice (choice-func x {!!} )
+             c2 : OD
+             c2 with p∨¬p ( (y : OD ) →  def c1 (od→ord y) ∧ (def x (od→ord  y)))
+             c2 | case1 _ = c1
+             c2 | case2 No =  {!!} -- minimal ( record { def = λ y → def c1 y ∧ def x y  } ) {!!}
+         Min1 : (x : OD) → Minimal x
+         Min1 x = (ε-induction {λ y → Minimal y  } induction x )
minimal : (x : OD  ) → ¬ (x == od∅ ) → OD
-         minimal x not = a-choice (minimal-choice x not )
-         -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+         minimal x not = min (Min1 x)
x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = is-in (minimal-choice x ne )
-         -- minimality (may proved by ε-induction )
+         x∋minimal x ne = x∋min (Min1 x) 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 = {!!}
+         minimal-1 x ne y = min-empty (Min1 x) ne y

```