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

changeset 49:7c23969befc9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Select
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 May 2019 20:48:20 +0900
parents 4fb2a239061d
children 7cb32d22528c
files ordinal-definable.agda
diffstat 1 files changed, 11 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Sat May 25 18:45:47 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 20:48:20 2019 +0900
@@ -173,7 +173,7 @@
     Replace : OD {n} → (OD {n} → OD {n} ) → OD {n}
     Replace X ψ = sup-od ψ
     Select : OD {n} → (OD {n} → Set n ) → OD {n}
-    Select X ψ = record { def = λ x → ψ ( ord→od x ) } 
+    Select X ψ = record { def = λ x → ( ( def X  x ) ∧ ψ ( ord→od x )) } 
     _,_ : OD {n} → OD {n} → OD {n}
     x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
     Union : OD {n} → OD {n}
@@ -228,13 +228,17 @@
          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∅)) → (x ∋ minimul x not) ∧
-            (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+         regularity :  (x : OD) (not : ¬ (x == od∅)) →
+            (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
-            reg0 : { x₁ : Ordinal} → def (Select (minimul x non , x) (λ x₂ → (minimul x non ∋ x₂) ∧ (x ∋ x₂))) x₁
-                    → def od∅ x₁
-            reg0 {x₁} t = {!!}
+            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))
+                ∧ def x (od→ord (ord→od y))) → Lift n ⊥
+            reg3 = {!!}
+            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
             reg1 :  Select (minimul x non , x) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
-            reg1 = record { eq→ = {!!} ; eq← = λ () }
+            reg1 = record { eq→ =  reg0 ; eq← = λ () }