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

comparison src/zorn.agda @ 1077:faa512b2425c

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 Fri, 16 Dec 2022 10:08:05 +0900
parents 7e047b46c3b2
children 2624f8a9f6ed
comparison
equal deleted inserted replaced
1076:7e047b46c3b2 1077:faa512b2425c
501 z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where 501 z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where
502 z47 : supf (supf x) ≡ supf x 502 z47 : supf (supf x) ≡ supf x
503 z47 = supf-idem x≤z sx≤z 503 z47 = supf-idem x≤z sx≤z
504 z45 : f (supf x) ≤ supf x 504 z45 : f (supf x) ≤ supf x
505 z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 505 z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
506
507 order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b
508 order0 {a} {b} {w} b≤z sa<sb sa≤z fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where
509 sa<b : supf a o< b
510 sa<b with x<y∨y≤x (supf a) b
511 ... | case1 lt = lt
512 ... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin
513 osuc (supf (supf a)) ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) sa≤z) ⟩
514 osuc (supf a) ≤⟨ osucc sa<sb ⟩
515 supf b ∎ )))) where open o≤-Reasoning O
506 516
507 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) 517 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f)
508 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 518 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
509 supf = ZChain.supf zc 519 supf = ZChain.supf zc
510 field 520 field
1233 ; zo≤sz = ? ; is-minsup = ? ; cfcs = ? } where 1243 ; zo≤sz = ? ; is-minsup = ? ; cfcs = ? } where
1234 mf : ≤-monotonic-f A f 1244 mf : ≤-monotonic-f A f
1235 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where 1245 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
1236 mf00 : * x < * (f x) 1246 mf00 : * x < * (f x)
1237 mf00 = proj1 ( mf< x ax ) 1247 mf00 = proj1 ( mf< x ax )
1238 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = 0<sufz 1248 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order ; 0<supfz = 0<sufz
1239 ; zo≤sz = ? ; is-minsup = is-minsup ; cfcs = cfcs } where 1249 ; zo≤sz = ? ; is-minsup = is-minsup ; cfcs = cfcs } where
1240 1250
1241 mf : ≤-monotonic-f A f 1251 mf : ≤-monotonic-f A f
1242 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where 1252 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
1243 mf00 : * x < * (f x) 1253 mf00 : * x < * (f x)
1576 ZChain.supf (pzc (ob<x lim (ordtrans u<x b<x) )) u ≡⟨ zeq _ _ (o<→≤ (osucc u<x)) (o<→≤ <-osuc) ⟩ 1586 ZChain.supf (pzc (ob<x lim (ordtrans u<x b<x) )) u ≡⟨ zeq _ _ (o<→≤ (osucc u<x)) (o<→≤ <-osuc) ⟩
1577 ZChain.supf (pzc (ob<x lim b<x )) u ∎ where open ≡-Reasoning 1587 ZChain.supf (pzc (ob<x lim b<x )) u ∎ where open ≡-Reasoning
1578 zc44 : FClosure A f (supf1 u) w 1588 zc44 : FClosure A f (supf1 u) w
1579 zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc 1589 zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
1580 1590
1591 order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
1592 order = ?
1593
1594
1581 --- 1595 ---
1582 --- the maximum chain has fix point of any ≤-monotonic function 1596 --- the maximum chain has fix point of any ≤-monotonic function
1583 --- 1597 ---
1584 1598
1585 SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x 1599 SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x