diff HOD.agda @ 180:11490a3170d4

new ordinal-definable
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 Jul 2019 14:05:32 +0900
parents aa89d1b8ce96
children
line wrap: on
line diff
--- a/HOD.agda	Sat Jul 20 08:21:54 2019 +0900
+++ b/HOD.agda	Sat Jul 20 14:05:32 2019 +0900
@@ -502,23 +502,20 @@
                          ≡⟨⟩
                             ly

-                    lemma2 : { lx : Nat } → lx < Suc lx  
-                    lemma2 {Zero} = s≤s z≤n
-                    lemma2 {Suc lx} = s≤s (lemma2 {lx})
                     lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
                     lemma z lt with  c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt
                     lemma z lt | case1 lz<ly with <-cmp lx ly
                     lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
-                    lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c =     -- (1)
+                    lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c =    -- ly(1)
                           subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
-                    lemma z lt | case1 lz<ly | tri> ¬a ¬b c =       -- z(a)
+                    lemma z lt | case1 lz<ly | tri> ¬a ¬b c =       -- lz(a)
                           subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
                     lemma z lt | case2 lz=ly with <-cmp lx ly
                     lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
-                    lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly       -- z(b)
+                    lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly        -- lz(b)
                     ... | eq = subst (λ k → ψ k ) oiso
                          (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
-                    lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly    -- z(c)
+                    lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly    -- lz(c)
                     ... | eq = lemma6 {ly} {Φ lx} {oy} lx=ly (sym (subst (λ k → lv (od→ord z) ≡  k) lemma1 eq)) where
                           lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
                           lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )