Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 744:d92ad9e365b6
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 21 Jul 2022 09:03:28 +0900 |
parents | 71556e611842 |
children | dc208a885e0c |
comparison
equal
deleted
inserted
replaced
743:71556e611842 | 744:d92ad9e365b6 |
---|---|
494 m03 = ⟪ proj1 ua , record { u = UChain.u (proj2 ua) ; u<x = m02 ; uchain = UChain.uchain (proj2 ua) } ⟫ | 494 m03 = ⟪ proj1 ua , record { u = UChain.u (proj2 ua) ; u<x = m02 ; uchain = UChain.uchain (proj2 ua) } ⟫ |
495 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b | 495 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b |
496 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab | 496 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab |
497 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b | 497 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b |
498 ... | tri≈ ¬a b=px ¬c = ? -- b = px case | 498 ... | tri≈ ¬a b=px ¬c = ? -- b = px case |
499 ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? } where | 499 ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order } where |
500 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u | 500 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u |
501 fcy<sup {u} {w} u<x fc = ? | 501 fcy<sup {u} {w} u<x fc = ZChain1.fcy<sup (prev (osuc u) (ob<x lim u<x)) <-osuc fc |
502 sup=u : {b : Ordinal} {ab : odef A b} → b o< x → | |
503 IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab → | |
504 ZChain.supf zc b ≡ b | |
505 sup=u {b} {ab} b<x is-sup = ZChain1.sup=u (prev (osuc b) (ob<x lim b<x)) <-osuc is-sup | |
506 order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → | |
507 FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b | |
508 order {b} b<x s<b fc = ZChain1.order (prev (osuc b) (ob<x lim b<x)) <-osuc s<b fc | |
502 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → | 509 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → |
503 b o< x → (ab : odef A b) → | 510 b o< x → (ab : odef A b) → |
504 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → | 511 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → |
505 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b | 512 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b |
506 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b | 513 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b |
507 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay ) | 514 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay ) |
508 ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) ) | 515 ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) ) |
509 (subst (λ k → * a < * k ) (sym b=y) a<b ) ) | 516 (subst (λ k → * a < * k ) (sym b=y) a<b ) ) |
510 ... | case2 y<b = chain-mono2 x (o<→≤ ob<x) o≤-refl m04 where | 517 ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where |
511 y<s : y << ZChain.supf zc b | 518 y<s : y << ZChain.supf zc b |
512 y<s = y<s | 519 y<s = y<s |
513 ob<x : osuc b o< x | |
514 ob<x with trio< (osuc b) x | |
515 ... | tri< a ¬b ¬c = a | |
516 ... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x } ) | |
517 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ ) | |
518 m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b | 520 m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b |
519 m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) ob<x) <-osuc fc | 521 m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) (ob<x lim b<x)) <-osuc fc |
520 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b | 522 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b |
521 m08 {sup1} {z1} s<b fc = ZChain1.order (prev (osuc b) ob<x) <-osuc s<b fc | 523 m08 {sup1} {z1} s<b fc = ZChain1.order (prev (osuc b) (ob<x lim b<x) ) <-osuc s<b fc |
522 m05 : b ≡ ZChain.supf zc b | 524 m05 : b ≡ ZChain.supf zc b |
523 m05 = sym (ZChain1.sup=u (prev (osuc b) ob<x) {_} {ab} <-osuc | 525 m05 = sym (ZChain1.sup=u (prev (osuc b) (ob<x lim b<x)) {_} {ab} <-osuc |
524 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ ob<x) o≤-refl lt )} ) -- ZChain on x | 526 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} ) -- ZChain on x |
525 m06 : ChainP A f mf ay (ZChain.supf zc) b b | 527 m06 : ChainP A f mf ay (ZChain.supf zc) b b |
526 m06 = record { fcy<sup = m07 ; csupz = subst (λ k → FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s } | 528 m06 = record { fcy<sup = m07 ; csupz = subst (λ k → FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s |
529 ; supfu=u = sym m05 } | |
527 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b | 530 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b |
528 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫ | 531 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫ |
529 | 532 |
530 --- | 533 --- |
531 --- the maximum chain has fix point of any ≤-monotonic function | 534 --- the maximum chain has fix point of any ≤-monotonic function |