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

changeset 599:d041941a8866

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
total done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jun 2022 02:10:15 +0900
parents 7a6d3f349395
children 71a1ed72cd21
files src/zorn.agda
diffstat 1 files changed, 6 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 14 01:50:31 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 02:10:15 2022 +0900
@@ -604,9 +604,12 @@
                      um02 i (fsuc j fc) = f-next zb ( um02 j fc )
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
-         ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy) {!!} {!!} (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
-         ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!}
-         ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) {!!} {!!} (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
+         ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)
+            (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+         ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+            (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
+         ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+            (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
          
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM