Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 285:313140ae5e3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 10 May 2020 09:25:13 +0900
parents a8f9c8a27e8d
children 4ae48eed654a
files LEMC.agda
diffstat 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