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

changeset 962:d594a8439174

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, 04 Nov 2022 19:19:51 +0900
parents 811135ad1904
children a8c3ccf8f9d9
files src/zorn.agda
diffstat 1 files changed, 12 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 04 18:55:44 2022 +0900
+++ b/src/zorn.agda	Fri Nov 04 19:19:51 2022 +0900
@@ -240,9 +240,9 @@
       ay : odef B y
       x=fy :  x ≡ f y 
 
--- record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
---    field
---       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+record IsSUP (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
+   field
+      x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
 record IsMinSUP (A B : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (xa : odef A x)     : Set n where
    field
@@ -409,7 +409,7 @@
    field
       supf :  Ordinal → Ordinal 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
-           → IsMinSUP A (UnionCF A f mf ay supf b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b 
+           → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b 
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -1388,9 +1388,10 @@
                    z23 : {z : Ordinal } → odef chain z → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z 
                    z23 {z} ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
                    z23 {z} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ = ⟪ au , ch-is-sup u z24 is-sup fc ⟫ where
-                       z26 : supf sp <= sp
-                       z26 = MinSUP.x≤sup sp1 ⟪ ?
-                           , ch-is-sup sp ? ? (init (ZChain.asupf zc) ? )  ⟫ 
+                       --  to prove sp is minsup , supf sp ≡ sp is necessary
+                       --  to prove supf s ≡ sp , sp is minsup is necessary
+                       z26 : supf sp ≡ sp
+                       z26 = ZChain.sup=u zc ? ? ⟪ record { x≤sup = ? } , ? ⟫
                        z25 : u <= sp
                        z25 = MinSUP.x≤sup sp1 ⟪ subst (λ k → odef A k) (ChainP.supu=u is-sup) (ZChain.asupf zc) 
                            , ch-is-sup u u<x is-sup (init (ZChain.asupf zc) (ChainP.supu=u is-sup))  ⟫ 
@@ -1539,9 +1540,8 @@
                    z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
                    z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
                    z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
-              is-sup :  IsMinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) (MinSUP.asm msp1)
-              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )
-                          ; minsup = ? ; not-hp = not-hasprev } 
+              is-sup :  IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc)  (MinSUP.asm msp1)
+              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) }
 
 
           not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d
@@ -1591,8 +1591,8 @@
                 -- ... | case1 eq =  MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup1) eq) refl fc )
                 -- ... | case2 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 ))
 
-          is-sup : IsMinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (cf nmx) (MinSUP.asm spd)
-          is-sup = record { x≤sup = z22 ; minsup = ? ; not-hp = not-hasprev } where
+          is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d)  (MinSUP.asm spd)
+          is-sup = record { x≤sup = z22 } where
                 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
                 z23 lt = MinSUP.x≤sup spd lt
                 z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →