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

changeset 50:7cb32d22528c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 May 2019 21:31:07 +0900
parents 7c23969befc9
children 83b13f1f4f42
files ordinal-definable.agda
diffstat 1 files changed, 4 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Sat May 25 20:48:20 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 21:31:07 2019 +0900
@@ -232,10 +232,11 @@
             (x ∋ minimul x not) ∧ (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 ( regularity x non ) =  minimul<x x non 
          proj2 ( regularity x non ) = reg1 where
-            reg3 : {y : Ordinal} → ((y ≡ od→ord (ord→od (mino (minord x non)))) ∨ (y ≡ od→ord x) )
-                ∧ ( def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 x eq)))))) (od→ord (ord→od y))
+            reg3 : {y : Ordinal} → ((y ≡ od→ord
+                        (ord→od (mino (minord x non)))) ∨ (y ≡ od→ord x) )
+                ∧ ( def (ord→od (mino (minord x non))) (od→ord (ord→od y))
                 ∧ def x (od→ord (ord→od y))) → Lift n ⊥
-            reg3 = {!!}
+            reg3 {y} = {!!}
             reg0 : {y : Ordinal} → def (Select (minimul x non , x)
                      (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
             reg0 {y} t = reg3 t