# HG changeset patch # User Shinji KONO # Date 1589013356 -32400 # Node ID a2991ce14ced1bec71dff01e8053396a4e6e7423 # Parent 197e0b3d39dcabd946dc270d682760de34e5b16c ... diff -r 197e0b3d39dc -r a2991ce14ced LEMC.agda --- 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