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

changeset 746:4a3ba4ad59d4

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 Thu, 21 Jul 2022 09:53:57 +0900
parents dc208a885e0c
children c35a5001a0f8
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jul 21 09:40:16 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 09:53:57 2022 +0900
@@ -365,8 +365,8 @@
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
-     -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
+ChainP-next A f mf {y} ay supf {x} {z} cp = record { y<s = ChainP.y<s cp ; supfu=u  = ChainP.supfu=u cp  
+     ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -461,7 +461,7 @@
                 m08 with proj2 m06
                 ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } = 
                           ch-init (f (HasPrev.y has-prev)) (fsuc _ fc) 
-                ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc) 
+                ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup (ChainP-next A f mf ay _ is-sup) (fsuc _ fc) 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where