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

changeset 1057:cd3237120dec

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lim
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 10 Dec 2022 07:01:34 +0900
parents 0dff7ab7a55f
children 12ce8d0224d2
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Dec 10 00:38:22 2022 +0900
+++ b/src/zorn.agda	Sat Dec 10 07:01:34 2022 +0900
@@ -1406,9 +1406,37 @@
           ... | tri≈ ¬a b ¬c = case1 refl
           ... | tri> ¬a ¬b c = case1 refl
 
-          supf-mono : {x y : Ordinal } → x o≤  y → supf1 x o≤ supf1 y
-          supf-mono {x} {y} x≤y with trio< y x
-          ... | tri< a ¬b ¬c = ?
+          sfpxo≤spu : {z : Ordinal } → supf1 z o≤ spu
+          sfpxo≤spu {z} with trio< z x
+          ... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
+          ... | tri≈ ¬a b ¬c = o≤-refl0 ?
+          ... | tri> ¬a ¬b c = o≤-refl0 ?
+
+          asupf : {z : Ordinal } → odef A (supf1 z)
+          asupf {z} with trio< z x
+          ... | tri< a ¬b ¬c = ZChain.asupf (pzc  (ob<x lim a)) 
+          ... | tri≈ ¬a b ¬c = MinSUP.as usup
+          ... | tri> ¬a ¬b c = MinSUP.as usup
+
+          supfmax : {z : Ordinal } → x o< z → supf1 z ≡ supf1 x
+          supfmax {z} x<z with trio< z x
+          ... | tri< a ¬b ¬c = ⊥-elim (o<> a x<z)
+          ... | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (sym b) x<z)
+          ... | tri> ¬a ¬b c = sym (sf1=spu o≤-refl)
+
+          supf-mono : {z y : Ordinal } → z o≤ y → supf1 z o≤ supf1 y
+          supf-mono {z} {y} z≤y with trio< y x
+          ... | tri< y<x ¬b ¬c = ? where
+               open o≤-Reasoning O
+               zc01 : supf1 z o≤ supf1 y -- ZChain.supf (pzc  (ob<x lim y<x)) y
+               zc01 with trio< z x
+               ... | tri< z<x ¬b ¬c = begin
+                  ZChain.supf (pzc  (ob<x lim z<x)) z ≤⟨ ZChain.supf-mono (pzc  (ob<x lim z<x)) z≤y  ⟩
+                  ZChain.supf (pzc  (ob<x lim z<x)) y ≡⟨ zeq _ _ ? ? ⟩
+                  ZChain.supf (pzc  (ob<x lim y<x)) y ≡⟨ sym (sf1=sf ?) ⟩
+                  supf1 y ∎ 
+               ... | tri≈ ¬a b ¬c = ?
+               ... | tri> ¬a ¬b c = ?
           ... | tri≈ ¬a b ¬c = ?
           ... | tri> ¬a ¬b c = ?