# HG changeset patch # User Shinji KONO # Date 1589070313 -32400 # Node ID 313140ae5e3d1793f8b2dc9055159658d63874e4 # Parent a8f9c8a27e8d9889bb6513b62f64aed7a3876823 clean up diff -r a8f9c8a27e8d -r 313140ae5e3d LEMC.agda --- a/LEMC.agda Sun May 10 09:19:32 2020 +0900 +++ b/LEMC.agda Sun May 10 09:25:13 2020 +0900 @@ -90,7 +90,7 @@ eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) } - record Minimal (x : OD) (ne : ¬ (x == od∅ ) ) : Set (suc n) where + record Minimal (x : OD) : Set (suc n) where field min : OD x∋min : x ∋ min @@ -100,20 +100,15 @@ -- -- 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 : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u ) + → (u : OD ) → (u∋x : u ∋ x) → Minimal u 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 + ... | case2 NP = min2 where p : OD p = record { def = λ y1 → def x y1 ∧ def u y1 } np : ¬ (p == od∅) @@ -124,10 +119,10 @@ y1 = a-choice y1choice y1prop : (x ∋ y1) ∧ (u ∋ y1) y1prop = is-in y1choice - min2 : Minimal u (∅< (proj2 y1prop)) + min2 : Minimal u 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 ) + Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u + Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } 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