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

changeset 505:5fcd2863317d

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 Wed, 13 Apr 2022 08:16:16 +0900
parents 5dd9cf0094d5
children dfcb98151273
files src/zorn.agda
diffstat 1 files changed, 14 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Apr 13 07:26:22 2022 +0900
+++ b/src/zorn.agda	Wed Apr 13 08:16:16 2022 +0900
@@ -137,18 +137,24 @@
       icy : odef (IChainSet {A} (me ax)) y 
       y>x : x o< y
 
+record IChainSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
+   field
+      y : Ordinal
+      A∋y : odef A y
+      y>x  : * x < * y
+
 -- finite IChain
 
 record InFiniteIChain (A : HOD) {x : Ordinal}  (ax : A ∋ * x) : Set n where
    field
       chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
-          → OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) cy)
+          → IChainSup> A ax
       
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field
       icy : odef (IChainSet {A} (me ax)) y  
-      c-finite : ¬ OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) icy)
+      c-finite : ¬ IChainSup> A ax
       
 record Maximal ( A : HOD )  : Set (suc n) where
    field
@@ -188,17 +194,17 @@
           zc6 : (ax : HOD) → elm x ≡ ax → (iy : IChain A (& y)) →  ic-connet iy  (& ax)
           zc6 ax refl iy = proj2 (proj1 zc3) iy
     ... | yes nogt with is-o∅ (& HG)
-    ... | no  nohg = case2 (case1 record { maximal = y ; A∋maximal = proj1 zc3 ; ¬maximal<x = zc4 } ) where
+    ... | no  finite-chain = case2 (case1 record { maximal = y ; A∋maximal = proj1 zc3 ; ¬maximal<x = zc4 } ) where
         y : HOD
-        y =  ODC.minimal O HG (λ eq → nohg (=od∅→≡o∅ eq))
+        y =  ODC.minimal O HG (λ eq → finite-chain (=od∅→≡o∅ eq))
         zc3 :  odef A (& y) ∧ IsFC A (d→∋ A (is-elm x) ) (& y)
-        zc3  = ODC.x∋minimal O HG  (λ eq → nohg (=od∅→≡o∅ eq))
+        zc3  = ODC.x∋minimal O HG  (λ eq → finite-chain (=od∅→≡o∅ eq))
         zc5 : odef (IChainSet {A} (me (d→∋ A (is-elm x) ))) (& y)
         zc5 = IsFC.icy (proj2 zc3)
-        zc6 :  odef (IChainSet {IChainSet (me (d→∋ A (is-elm x)))} (me (d→∋ (IChainSet (me (d→∋ A (is-elm x)))) (IsFC.icy (proj2 zc3))))) (& y)
-        zc6 = ⟪ {!!} , {!!} ⟫
         zc4 : {z : HOD} → A ∋ z → ¬ (y < z)
-        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; icy =  {!!} ; y>x = {!!} }
+        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; A∋y =  az ; y>x = {!!} } where
+            zc6 : elm x < z
+            zc6 = {!!}
     ... | yes  nohg = case2 (case2 {!!} )