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

changeset 792:150e1c7097ce

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 Thu, 04 Aug 2022 06:59:40 +0900
parents f4450bc95699
children bcc241fbb390
files src/zorn.agda
diffstat 1 files changed, 15 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Aug 03 16:04:51 2022 +0900
+++ b/src/zorn.agda	Thu Aug 04 06:59:40 2022 +0900
@@ -744,16 +744,23 @@
                  UnionCF⊆ ⟪ as , ch-init fc ⟫ = UnionCF⊆ ⟪ as , ch-init fc ⟫ 
                  UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1  }  fc ⟫ with trio< u px
                  ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫  where
-                     order1 :  {s z1 : Ordinal} → supf1 s o< supf0 u → FClosure A f (supf1 s) z1 
-                        → (z1 ≡ supf0 u) ∨ (z1 << (supf0 u))
-                     order1 {s} {z1} = o1 {s} {z1}
                      order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
                         → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                     order0 {s} {z1} with trio< s px
-                     ... | tri< a ¬b ¬c = o1 {s} {z1}
-                     ... | tri≈ ¬a b ¬c = o1 {s} {z1}
-                     ... | tri> ¬a ¬b c = ?
-                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = ? } fc ⟫ 
+                     order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
+                     ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
+                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
+                     ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
+                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
+                     ... | tri> ¬a ¬b c | record {eq = eq1} = ?
+                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫ where
+                     order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
+                        → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
+                     order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
+                     ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
+                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
+                     ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
+                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
+                     ... | tri> ¬a ¬b c | record {eq = eq1} = ?
                  ... | tri> ¬a ¬b c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = fcy<sup ; order = order } fc0 ⟫  where
                      --    px o< u , u o< osuc x → u ≡ x
                      --    supf0 x ≡ sp1 ≡ x