Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 974:9bfe54cd9fb9
csupf removal?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 07 Nov 2022 22:01:54 +0900 |
| parents | 2a67cae517d8 |
| children | 1e88cce74699 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 15 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Nov 07 17:56:03 2022 +0900 +++ b/src/zorn.agda Mon Nov 07 22:01:54 2022 +0900 @@ -1173,6 +1173,21 @@ odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m ? ? + csupf10 : {z1 : Ordinal } → supf1 z1 o< supf1 x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) + csupf10 {z1} sz<sx = ⟪ asupf1 , ch-is-sup z1 sz<sx cs01 (init asupf1 refl ) ⟫ where + cs01 : ChainP A f mf ay supf1 z1 + cs01 = record { fcy<sup = fcy<sup ; order = ? ; supu=u = ? } where + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 z1) ∨ (z << supf1 z1) + fcy<sup {z} fc with trio< z1 px + ... | tri< a ¬b ¬c = ZChain.fcy<sup zc (o<→≤ a) fc + ... | tri≈ ¬a b ¬c = ZChain.fcy<sup zc (o≤-refl0 b) fc + ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 (case1 ⟪ A∋fc _ fc , ch-init fc ⟫) + order : {s w : Ordinal} → (lt : supf1 s o< supf1 z1) → FClosure A f (supf1 s ) w → (w ≡ supf1 z1 ) ∨ ( w << supf1 z1 ) + order {s} {z1} lt fc with trio< z1 px + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 ? + csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf1 {z1} sz1<x = csupf2 where -- z1 o< px → supf1 z1 ≡ supf0 z1