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

changeset 613:7c5a922931e5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Jun 2022 21:45:33 +0900
parents 099ca2fea51c
children eb9cf48f530a d0938f220648
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jun 17 21:20:24 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 21:45:33 2022 +0900
@@ -671,14 +671,9 @@
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za)  ⊆' ZChain.chain (ZChain1.zc zb)
-         u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain (ZChain1.zc za)) i → odef (chain (ZChain1.zc zb)) i } uind i zai where
-            open ZChain
-            uind :  (i : Ordinal)
-                 → ((j : Ordinal) → j o< i →  odef (chain (ZChain1.zc za)) j → odef (chain (ZChain1.zc zb)) j)
-                 → odef (chain (ZChain1.zc za)) i → odef (chain (ZChain1.zc zb)) i
-            uind i previ zai = um01 where
-                um01 : odef (chain (ZChain1.zc zb)) i
-                um01 = {!!}
+         u-mono a b b<x a≤b za zb {i} zai = ZChain1.chain-mono zb a≤b <-osuc (uz01 zai) where
+              uz01 : odef (* (SupF.chain (ZChain1.supf za a))) i → odef (* (SupF.chain (ZChain1.supf zb a))) i
+              uz01 = {!!}
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)