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

changeset 596:f484cff027e4

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 Tue, 14 Jun 2022 00:25:59 +0900
parents 96f377d87427
children 2595d2f6487b
files src/zorn.agda
diffstat 1 files changed, 10 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jun 13 23:11:08 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 00:25:59 2022 +0900
@@ -248,7 +248,7 @@
 
 data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where
       Finit :  {z : Ordinal} → z ≡ y  → Fc∨sup A ay f z
-      Fc  :  {p x : Ordinal} → p o< x → Fc∨sup A ay f p  → FChain A f p x →  Fc∨sup A ay f x
+      Fc  :  {p x : Ordinal} → p o< osuc x → Fc∨sup A ay f p  → FChain A f p x →  Fc∨sup A ay f x
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -584,27 +584,27 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
-         u-mono :  ( a b : Ordinal ) → b o< x → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
-         u-mono a b b<x = TransFinite {λ a → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b)
+         u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
+         u-mono a b b<x = TransFinite {λ a → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b)
              → ZChain.chain za  ⊆' ZChain.chain zb } uind a where
             open ZChain
             uind :  (a : Ordinal)
-                 → ((c : Ordinal) → c o< a →  c o< b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
-                 → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb
-            uind a previ a<b za zb {i} zai = um01 where
+                 → ((c : Ordinal) → c o< a →  c o< osuc b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
+                 → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb
+            uind a previ a≤b za zb {i} zai = um01 where
                 FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i 
                 FC = fc∨sup za zai 
-                FCb : Fc∨sup A (chain⊆A zb (chain∋x zb)) f i 
-                FCb =  {!!}
+                -- y≤fc : {a p : Ordinal} → Fc∨sup A p f i → * y ≤ * p
+                -- y≤fc =  {!!}
                 um01 : odef (chain zb) i
                 um01 with FC
                 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
-                ... | Fc {p} {i} p<i pFC fc with initial za zai
+                ... | Fc {p} {i} p≤i pFC fc with initial za zai
                 ... | case1 y=i = subst (λ k → odef (chain zb) k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=i)) ( chain∋x zb )
                 ... | case2 y<i with (FChain.fc∨sup fc) 
                 ... | case1 fc = um02 i fc where
                      um02 : (i : Ordinal) → FClosure A f p i → odef (chain zb) i
-                     um02 i (init ap i=p ) = {!!}
+                     um02 i (init ap i=p ) = subst (λ k → odef (chain zb) k ) (sym i=p) (previ a {!!} {!!} za zb {!!} ) where
                      um02 i (fsuc j fc) = f-next zb ( um02 j fc )
                 ... | case2 sup = {!!}
                 -- is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} y<i where