### diff LEMC.agda @ 279:197e0b3d39dc

...
author Shinji KONO Sat, 09 May 2020 16:41:40 +0900 d9d3654baee1 a2991ce14ced
line wrap: on
line diff
```--- a/LEMC.agda	Sat May 09 09:40:18 2020 +0900
+++ b/LEMC.agda	Sat May 09 16:41:40 2020 +0900
@@ -84,4 +84,17 @@
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
+         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 )
+         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 )
+         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 = {!!}
+
+
+
```