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

changeset 510:ec84dce16697

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 Apr 2022 18:27:04 +0900
parents 72ea26339f66
children 361021fe53aa
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Apr 15 16:46:54 2022 +0900
+++ b/src/zorn.agda	Fri Apr 15 18:27:04 2022 +0900
@@ -167,13 +167,23 @@
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
           → IChainSup> A ax
 
+open import Data.Nat hiding (_<_) 
+import Data.Nat.Properties as NP
+open import nat
+
 data Chain (A : HOD) (next : (x : Ordinal ) → odef A x → Ordinal ) : ( x : Ordinal  ) → Set n where
-     cfirst : {x : Ordinal } → odef A x → Chain A next x
-     csuc : {x : Ordinal } → (ax : odef A x ) → Chain A next x → Chain A next (next x ax )
+     cfirst : (x : Ordinal ) → odef A x → Chain A next x
+     csuc : (x : Ordinal ) → (ax : odef A x ) → Chain A next x → Chain A next (next x ax )
 
 ChainClosure : (A : HOD) →  (next : (x : Ordinal ) → odef A x → Ordinal ) → HOD
 ChainClosure A  next = record { od = record { def = λ x → Chain A next x } ; odmax = {!!} ; <odmax = {!!} }
 
+cton0 : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal )  {y : Ordinal } → Chain A next y → ℕ
+cton0 A next (cfirst _ x) = zero
+cton0 A next (csuc x ax z) = suc (cton0 A next z)
+cton : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → Element (ChainClosure A next) → ℕ
+cton A next y = cton0 A next (is-elm y)
+
 InFCSet : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → (ifc : InFiniteIChain A ax ) → HOD
 InFCSet A ax ifc =  ChainClosure (IChainSet {A} (me ax)) (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 
@@ -186,8 +196,13 @@
    ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
     IPO : IsPartialOrderSet (InFCSet A ax ifc )
     IPO = ⊆-IsPartialOrderSet record { incl = λ {x} lt → {!!} } PO
+    cnext :  (y : Ordinal ) → odef (IChainSet {A} (me ax)) y → Ordinal
+    cnext y ay = IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay  )
     cmp : Trichotomous _ _ 
-    cmp x y = {!!}
+    cmp x y with NP.<-cmp (cton (IChainSet {A} (me ax)) cnext x) (cton (IChainSet {A} (me ax)) cnext y)
+    ... | tri< a ¬b ¬c = {!!}
+    ... | tri≈ ¬a b ¬c = {!!}
+    ... | tri> ¬a ¬b c = {!!}
 
       
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where