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

changeset 56:aad8cdce8845

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
almost ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 May 2019 00:07:23 +0900
parents 9c0a5e28a572
children 419688a279e0
files ordinal-definable.agda
diffstat 1 files changed, 5 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Mon May 27 23:45:56 2019 +0900
+++ b/ordinal-definable.agda	Tue May 28 00:07:23 2019 +0900
@@ -332,7 +332,11 @@
          proj2 ( regularity x non ) = reg1 where
             reg2 : {y : Ordinal} → ( def (minimul x non) y ∧ (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥ 
             reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
-            ... | p1 | p2 | p3 = {!!}
+            ... | p1 | p2 | p3  with is-∋ x ( ord→od y)
+            reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 )                         --  ¬ x ∋ ord→od y     empty x case
+            reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul x non) (ord→od y)
+            reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 )                 --  minimum contains nothing q.e.d.
+            reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!}
             reg0 : {y : Ordinal {suc n}} → Minimumo (od→ord x) → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
             reg0 {y} m t with trio< y (mino (minord x non)) 
             reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} ( record {
@@ -355,9 +359,3 @@
             reg1 :  Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
             reg1 = record { eq→ =  reg0 (minord x non) ; eq← = λ () }
 
-
---               (o<-subst {suc n} {y} (c<→o< {suc n} (def-subst {suc n} (proj1 t ) {!!} {!!} )) {!!} {!!} )
---            c<> {n} (o<→c< {suc n} {mino (minord x  non)} {y} (case2 lto))
---                  (def-subst {suc n} {ord→od (mino (minord x  non))} {y} lt refl refl ) --            lemma y ( mino (minord x non) )
---                 (def-subst {suc n} {ord→od y} {mino (minord x  non)} (proj1 t) refl (sym diso))
---                     {!!} where