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

changeset 327:cde56f704eac

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 Sun, 05 Jul 2020 04:09:00 +0900
parents feeba7fd499a
children 72f3e3b44c27
files OD.agda
diffstat 1 files changed, 2 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Sun Jul 05 03:45:41 2020 +0900
+++ b/OD.agda	Sun Jul 05 04:09:00 2020 +0900
@@ -329,10 +329,8 @@
             lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt }
         lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
         lemma3 {x} = od⊆→o≤ lemma1
-        lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x))
-        lemma4 {x} = ordtrans (<odmax (u x , u x) (case2 refl)) 
-           (subst (λ k → k o< osuc (osuc (od→ord x))) (omax≡ _ _ refl) ( -- odmax (u x , u x) o< osuc (osuc (od→ord x))
-            osucc {!!} )) -- osuc (od→ord (u x)) o<  osuc (osuc (od→ord x))
+        lemma6 : {x y : HOD} → y ≡ u x → HOD
+        lemma6 {x} _ = x
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
         lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →