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

changeset 715:e4587714c376

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, 15 Jul 2022 14:14:53 +0900
parents e1ef5e6961ce
children b0cad3ec7da0
files src/OrdUtil.agda src/zorn.agda
diffstat 2 files changed, 20 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/OrdUtil.agda	Fri Jul 15 12:35:59 2022 +0900
+++ b/src/OrdUtil.agda	Fri Jul 15 14:14:53 2022 +0900
@@ -47,6 +47,12 @@
 ... | case1 eq = o<¬≡ (sym eq) (proj1 P) 
 ... | case2 lt = o<> lt (proj1 P) 
 
+b<x→0<x : { p b : Ordinal } → p o< b →  o∅  o< b
+b<x→0<x {p} {b} p<b with trio< o∅ b
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a 0=b ¬c = ⊥-elim ( ¬x<0 ( subst (λ k → p o< k) (sym 0=b) p<b ) )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
--- a/src/zorn.agda	Fri Jul 15 12:35:59 2022 +0900
+++ b/src/zorn.agda	Fri Jul 15 14:14:53 2022 +0900
@@ -621,9 +621,21 @@
                       ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
                       ... | tri≈ ¬a b ¬c = ? -- ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans b (sym &iso) )  (ChainP.au is-sup ) ))
                       ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
-                ... | tri≈ ¬a b=px ¬c = ? -- ⊥-elim ( noapx (subst (λ k → odef A k ) (trans b=px (sym &iso))  ab ) )
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
-                -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
+                ... | tri≈ ¬a b=px ¬c = zc15 where
+                       zc14 : f (HasPrev.y pr) ≡ b
+                       zc14 = begin f (HasPrev.y pr)  ≡⟨ sym (HasPrev.x=fy pr) ⟩ 
+                          & (* px)                   ≡⟨ &iso ⟩ 
+                          px                         ≡⟨ sym b=px ⟩ 
+                          b ∎ where open   ≡-Reasoning 
+                       zc15 : odef pchain b
+                       zc15 with  ZChain.f-next zc (HasPrev.ay pr) 
+                       ... | ⟪ az , record  { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ 
+                           = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case2 refl 
+                              ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc)  } ⟫ 
+                       ... | ⟪ az , record  { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ 
+                           = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case1 (b<x→0<x b<x ) 
+                            ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc) } ⟫ 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal