Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 954:e43a5cc72287

IsSUP is now min sup

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 02 Nov 2022 13:53:10 +0900
parents	dfb4f7e9c454
children	bc27df170a1e

comparison

equal deleted inserted replaced

-:dfb4f7e9c454
+:e43a5cc72287
 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 )
+minsup : { sup1 : Ordinal } → odef A sup1
+→  ( {z : Ordinal  } → odef B z → (z ≡ sup1 ) ∨ (z << sup1 ))  → x o≤ sup1
 record SUP ( A B : HOD )  : Set (Level.suc n) where
 field
 sup : HOD
 as : A ∋ sup
 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
 m05 : ZChain.supf zc b ≡ b
 m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz) }  , m04 ⟫
+⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz)
+; minsup = m07 }  , m04 ⟫ where
+m10 : {s : Ordinal }  →  (odef A s )
+→  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) )
+→    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
+m10 = ?
+m07 :  {sup1 : Ordinal} → odef A sup1 → ({z : Ordinal} →
+odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ sup1) ∨ (z << sup1)) → b o≤ sup1
+m07 {s} as min = IsSup.minsup (proj2 is-sup) as (m10 as min)
 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
 m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
 m09 {s} {z} s<b fcz = order b<A s<b fcz
 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
 ; x=fy = HasPrev.x=fy nhp } )
 m05 : ZChain.supf zc b ≡ b
 m05 = ZChain.sup=u zc ab (o<→≤  m09)
-⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫    -- ZChain on x
+⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )
+; minsup = ? } , m04 ⟫    -- ZChain on x
 m06 : ChainP A f mf ay supf b
 m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
 uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
 --
 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
 → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
 ind f mf {y} ay x prev with Oprev-p x
-... | yes op = zc4 where
+... | yes op = zc41 where
 --
 -- we have previous ordinal to use induction
 --
 px = Oprev.oprev op
 zc : ZChain A f mf ay (Oprev.oprev op)
 ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
 ... | case1 eq = case2 eq
 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
-zc41 : supf0 px o< x →  ZChain A f mf ay x
+--
-zc41 sfpx<x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
+-- find the next value of supf
+--
+pchainpx : HOD
+pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z )
+∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
+zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A
+zc00 {z} (case1 lt) = z07 lt
+zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc )
+zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b
+zc02 {a} {b} ca fb = zc05 fb where
+zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px
+zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl
+zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b
+zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
+... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
+... | case2 lt = <-ftrans (zc05 fb) (case2 lt)
+zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl)
+(subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
+... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
+... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt )
+ptotal : IsTotalOrderSet pchainpx
+ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso
+(chain-total A f mf ay supf0 (proj2 a) (proj2 b))
+ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
+... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
+eq1 : a0 ≡ b0
+eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
+lt1 : a0 < b0
+lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
+... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
+eq1 : a0 ≡ b0
+eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
+lt1 : a0 < b0
+lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b)
+pcha : pchainpx ⊆' A
+pcha (case1 lt) = proj1 lt
+pcha (case2 fc) = A∋fc _ f mf fc
+sup1 : MinSUP A pchainpx
+sup1 = minsupP pchainpx pcha ptotal
+sp1 = MinSUP.sup sup1
+--
+--     supf0 px o≤ sp1
+--
+zc41 : ZChain A f mf ay x
+zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
+zc41 | (case2 sfpx<sp1) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
---  supf0 px is included by the chain
+--  supf0 px is included by the chain of sp1
 --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
 --  supf1 x ≡ sp1, which is not included now
-pchainpx : HOD
-pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z )
-∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
-zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A
-zc00 {z} (case1 lt) = z07 lt
-zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc )
-zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → odef A z
-zc01 {z} (case1 lt) = proj1 lt
-zc01 {z} (case2 fc) = ( A∋fc (supf0 px) f mf fc )
-zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b
-zc02 {a} {b} ca fb = zc05 fb where
-zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px
-zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl
-zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b
-zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
-... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
-... | case2 lt = <-ftrans (zc05 fb) (case2 lt)
-zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl)
-(subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
-... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
-... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt )
-ptotal : IsTotalOrderSet pchainpx
-ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso
-(chain-total A f mf ay supf0 (proj2 a) (proj2 b))
-ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
-... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
-eq1 : a0 ≡ b0
-eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
-... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
-lt1 : a0 < b0
-lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
-... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
-eq1 : a0 ≡ b0
-eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
-... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
-lt1 : a0 < b0
-lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b)
-pcha : pchainpx ⊆' A
-pcha (case1 lt) = proj1 lt
-pcha (case2 fc) = A∋fc _ f mf fc
-sup1 : MinSUP A pchainpx
-sup1 = minsupP pchainpx pcha ptotal
-sp1 = MinSUP.sup sup1
 supf1 : Ordinal → Ordinal
 supf1 z with trio< z px
 ... | tri< a ¬b ¬c = supf0 z
 ... | tri≈ ¬a b ¬c = supf0 z
 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
 s≤px : s o≤ px
 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px  ⟫ )
 zc12 {z} (case2 fc) = zc21 fc where
+zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px )
+zc20 = ?
 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
 zc21 {z1} (fsuc z2 fc ) with zc21 fc
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
-zc21 (init asp refl ) with  osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
+zc21 (init asp refl ) with  zc20
 ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px zc18
 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
 zc15 : supf1 px ≡ px
 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
 zc18 : supf1 px o< supf1 x
 csupf17 (init as refl ) = ZChain.csupf zc sf<px
 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
 ... | case2 sfp<px  with ZChain.csupf zc sfp<px --  odef (UnionCF A f mf ay supf0 px) (supf0 px)
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫
-... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ?
+... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18
 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫  where
 z10 :  {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc)
 z11  : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1
 → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u )
 s≤px = ordtrans s<u ? -- (o<→≤ u<x)
 lt0 : supf0 s o< supf0 u
 lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt
 z12 : supf1 u ≡ u
 z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup)
+zc18 : supf1 u o< supf1 x
+zc18 = ?
 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
 field
 ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫  )  where
 --- supf1 z1 ≡ px , z1 o< px ,  px ≡ supf0 z1 o< supf0 px o< x
 cs05 : px o< supf0 px
 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
 cs06 : supf0 px o< osuc px
-cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x
+cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ?
 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ?
 -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
-zc4 : ZChain A f mf ay x     --- x o≤ supf px
+zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
-zc4 with trio< x (supf0 px)
-... | tri> ¬a ¬b c = zc41 c
-... | tri≈ ¬a b ¬c = ?
-... | tri< a ¬b ¬c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
 --  supf0 px not is included by the chain
 --     supf1 x ≡ supf0 px because of supfmax
 ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
 zc12 : supf0 x ≡ u1
 zc12 = subst  (λ k → supf0 k ≡ u1) eq ?
 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
 zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
-; is-sup = record { x≤sup = x≤sup } }
+; is-sup = record { x≤sup = x≤sup ; minsup = ? } }
 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
 eq : u1 ≡ x
 eq with trio< u1 x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
 ... | tri≈ ¬a b ¬c = b
 zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
 zc37 = record { sup = ? ; asm = ? ; x≤sup = ? }
 sup=u : {b : Ordinal} (ab : odef A b) →
 b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
 sup=u {b} ab b≤x is-sup with trio< b px
-... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫
+... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫
-... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫
+... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫
 ... | tri> ¬a ¬b px<b = zc31 ? where
 zc30 : x ≡ b
 zc30 with osuc-≡< b≤x
 ... | case1 eq = sym (eq)
 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
 zcsup with zc30
 ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt →
-IsSup.x≤sup (proj1 is-sup) ?} }
+IsSup.x≤sup (proj1 is-sup) ? ; minsup = ? } }
 zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
 zc31 (case1 ¬sp=x) with zc30
 ... | refl = ⊥-elim (¬sp=x zcsup )
 zc31 (case2 hasPrev ) with zc30
 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
 z13 :  * (& s) < * sp
 z13 with x≤sup ( ZChain.chain∋init zc )
 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
 z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
-z19 = record {   x≤sup = z20 }  where
+z19 = record {   x≤sup = z20 ; minsup = ? }  where
 z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
 z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy)
 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
 ztotal : IsTotalOrderSet (ZChain.chain zc)
 sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
 sc=c : supf mc ≡ mc
 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
 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 )}
+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-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx)
 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where
 z30 : * mc < * (cf nmx mc)
 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
 z31 : ( * (cf nmx mc)  ≡  * mc ) ∨ ( * (cf nmx mc) < * mc )
 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 : 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
+is-sup = record { x≤sup = z22 ; minsup = ? } 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 →
 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
 z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where

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

comparison src/zorn.agda @ 954:e43a5cc72287