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

changeset 42:4d5fc6381546

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
regurality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 May 2019 10:28:02 +0900
parents b60db5903f01
children 0d9b9db14361
files ordinal-definable.agda
diffstat 1 files changed, 10 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Fri May 24 08:21:41 2019 +0900
+++ b/ordinal-definable.agda	Fri May 24 10:28:02 2019 +0900
@@ -94,10 +94,6 @@
   field
      mino : Ordinal {n}
      min<x :  mino o< x
-  defmin : def ( ord→od x ) mino
-  defmin = lemma ( o<→c< min<x ) where
-     lemma : def (ord→od x) (od→ord ( ord→od mino))  → def ( ord→od x ) mino
-     lemma m< = def-subst {n} {ord→od x} m< refl diso
 
 ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x
 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
@@ -229,13 +225,17 @@
          minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} 
          minimul x  not = ord→od ( mino (minord x not))
          minimul<x : (x : OD {n} ) →  (not :  ¬ x ≡ od∅ ) → x ∋ minimul x not
-         minimul<x x not = lemma0 where
-            lemma :  def x (mino (minord x not))
-            lemma = def-subst (defmin (minord x not)) oiso refl
-            lemma0 : def x (od→ord (ord→od (mino (minord x not))))
-            lemma0 = def-subst {n} {x} lemma refl {!!}
+         minimul<x x not = lemma0 (min<x (minord x not)) where
+            lemma0 : mino (minord x not)  o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
+            lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
          regularity : (x : OD) → (not : ¬ x ≡ od∅ ) →
                 Lift (suc n) (x ∋ minimul x not ) ∧
                 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
          proj1 ( regularity x non ) = lift ( minimul<x x non )
-         proj2 ( regularity x non ) = {!!}
+         proj2 ( regularity x non ) = cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) )   where
+            lemma : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z 
+            lemma z with (minimul x non ∋ (ord→od z)) | x ∋ (ord→od z)
+            ... | s | t = {!!}
+            lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z ≡ Lift n ⊥ 
+            lemma0 = {!!}
+