### changeset 285:313140ae5e3d

clean up
author Shinji KONO Sun, 10 May 2020 09:25:13 +0900 a8f9c8a27e8d 4ae48eed654a LEMC.agda 1 files changed, 7 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
```--- 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 ```