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

comparison src/zorn.agda @ 891:9fb948dac666

u < supf z

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 05 Oct 2022 13:13:35 +0900
parents	3eaf3b8b1009
children	f331c8be2425

comparison

equal deleted inserted replaced

-:3eaf3b8b1009
+:9fb948dac666
 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-x≤supfx : {x : Ordinal } → x o≤ supf z → x o≤ supf x
+x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x
+supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x)
-supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (M→S supf (minsup x≤z) ))
+supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
 csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
 chain : HOD
 chain = UnionCF A f mf ay supf z
 chain⊆A : chain ⊆' A
 chain⊆A = λ lt → proj1 lt
 sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
 sup {x} x≤z = M→S supf (minsup x≤z)
-supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
+-- supf-sup<minsup : {x : Ordinal } → (x≤z : x o≤ z) → & (SUP.sup (M→S supf (minsup x≤z) )) o≤ supf x ... supf-mono
-supf-is-minsup {x} x≤z = trans (supf-is-sup x≤z) &iso
 chain∋init : odef chain y
 chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
 f-next : {a : Ordinal} → odef chain a → odef chain (f a)
 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
 ... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) )
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
-supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
+supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-minsup b≤z)) ( MinSUP.asm ( minsup b≤z ) )
 -- supf-idem : {x : Ordinal } → supf x o≤ z  → supf (supf x) ≡ supf x
 -- supf-idem {x} sx≤z = sup=u (supf∈A ?) sx≤z ?
 fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
+fcy<sup  {u} {w} u≤z fc with MinSUP.x<sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
-... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
+... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans ? (sym (supf-is-minsup u≤z ) ) ))
-... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
+... | case2 lt = case2 ? -- (subst (λ k → * w < k ) ? )-- (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-minsup u≤z ))) ) lt )
 -- ordering is not proved here but in ZChain1
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 supf = ZChain.supf zc
 field
-is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  b o< supf z  → (ab : odef A b)
+is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  b o< z  → (ab : odef A b)
 → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab
 → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 field
 SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
 chain-mono1 :  {a b c : Ordinal} → (ZChain.supf zc a) o≤ (ZChain.supf zc b)
 → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
 chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
-b o< ZChain.supf zc x → (ab : odef A b) →
+b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab ,
 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 order {b} {s} {z1} b<z ss<sb fc = zc04 where
-zc00 : ( * z1  ≡  SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) )
+zc00 : ( z1  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
-zc00 = SUP.x<sup (ZChain.sup zc (o<→≤  b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
+zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) ? -- (csupf-fc (o<→≤ b<z) ss<sb fc )
 -- supf (supf b) ≡ supf b
 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
 zc04 with zc00
-... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z))  ) (cong (&) eq) )
+... | case1 eq = ? -- case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) (cong (&) eq) )
-... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) )))  lt )
+... | case2 lt = ? -- case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) ) )))  lt )
 zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
 zc1 x prev with Oprev-p x
 ... | yes op = record { is-max = is-max } where
 px = Oprev.oprev op
 zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
-b o< ZChain.supf zc x → (ab : odef A b) →
+b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b
 is-max {a} {b} ua b<x ab P a<b | case2 is-sup
-= ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+= ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
 b<A : b o< & A
 b<A = z09 ab
 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 ? (HasPrev.ay  nhp)
 ; x=fy = HasPrev.x=fy nhp } )
 m09 {s} {z} s<b fcz = order b<A s<b fcz
 m06 : ChainP A f mf ay supf b
 m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
 ... | no lim = record { is-max = is-max }  where
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-b o< ZChain.supf zc x → (ab : odef A b) →
+b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b
 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-... | case2 y<b = chain-mono1 ?
+... | case2 y<b = ⟪ ab , ch-is-sup b m10 m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
-⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
+m10 : b o< ZChain.supf zc x
+m10 = ordtrans<-≤ b<x ( ZChain.x≤supfx zc ? )
 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
 m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
 m08 : {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
 m08 {s} {z1} s<b fc = order m09 s<b fc
 fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc  ))
 fixpoint f mf zc = z14 where
 chain = ZChain.chain zc
 sp1 = sp0 f mf as0 zc
-z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< ZChain.supf zc (& A) → (ab : odef A b )
+z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b )
 →  HasPrev A chain b f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
 → * a < * b  → odef chain b
 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+z21 : & (SUP.sup sp1) o< & A
+z21 = c<→o< ( SUP.as sp1)
+--  ZChain.supf zc (& A) o≤ & (SUP.sup sp1)  ( minimality )
 z11 : & (SUP.sup sp1) o< ZChain.supf zc (& A)
 z11 = ? -- c<→o< ( SUP.as sp1)
 z12 : odef chain (& (SUP.sup sp1))
 z12 with o≡? (& s) (& (SUP.sup sp1))
 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.as sp1)
+... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1)
 (case2 z19 ) z13 where
 z13 :  * (& s) < * (& (SUP.sup sp1))
 z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
 zc01 {z} (case1 lt) = proj1 lt
 zc01 {z} (case2 fc) = ( A∋fc px f mf fc )
 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 (supf0 px) a → FClosure A f px b → a <= b
 zc02 {a} {b} ca fb = zc05 fb where
-zc06 : & (SUP.sup (ZChain.sup zc o≤-refl)) ≡ px
+zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
-zc06 = trans (sym ( ZChain.supf-is-sup zc o≤-refl )) (sym sfpx=px)
+zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) (sym sfpx=px)
 zc05 : {b : Ordinal } → FClosure A f px b → a <= b
 zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc 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 SUP.x<sup (ZChain.sup zc o≤-refl)
+zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl)
 ? -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 ? k) (sym &iso) ca )
-... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 (cong (&) eq))
+... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 ? )-- (cong (&) eq))
-... | case2 lt = case2 (subst (λ k → (* a) < k ) (trans (sym *iso) (cong (*) zc06)) lt)
+... | case2 lt = case2 (subst (λ k → (* a) < k ) ? ? ) -- (trans (sym *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
 -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
 csupf17 (init as refl ) = ZChain.csupf zc sf<px
 csupf17 (fsuc x fc) = ? -- ZChain.f-next zc ? -- (csupf17 fc)
-x≤supfx1 : {z : Ordinal} → z o≤ supf1 x → z o≤ supf1 z
+x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z
 x≤supfx1 {z} z≤x with trio< z (supf1 z) --  supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px
 ... | tri< a ¬b ¬c = o<→≤ a
 ... | tri≈ ¬a b ¬c = o≤-refl0 b
 ... | tri> ¬a ¬b c with trio< z px
 ... | tri< a ¬b ¬c = ZChain.x≤supfx zc ?
 supf0 u1 ≡⟨ su=z ⟩
 z ∎ where open ≡-Reasoning
 zc13 : odef pchain z
 zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) )
 zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc)
 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
 field
-tsup : SUP A (UnionCF A f mf ay supf0 z)
+tsup : MinSUP A (UnionCF A f mf ay supf1 z)
-tsup=sup : supf0 z ≡ & (SUP.sup tsup )
+tsup=sup : supf1 z ≡ MinSUP.sup tsup
 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
 sup {z} z≤x with trio< z px
-... | tri< a ¬b ¬c = record { tsup = ZChain.sup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-sup zc (o<→≤ a) }
+... | tri< a ¬b ¬c = ? -- jrecord { tsup = ZChain.minsup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-minsup zc (o<→≤ a) }
-... | tri≈ ¬a b ¬c = record { tsup = ZChain.sup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-sup zc (o≤-refl0 b) }
+... | tri≈ ¬a b ¬c = ? -- record { tsup = ZChain.minsup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-minsup zc (o≤-refl0 b) }
 ... | tri> ¬a ¬b px<z = zc35 where
 zc30 : z ≡ x
 zc30 with osuc-≡< z≤x
 ... | case1 eq = eq
 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
 zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
 zc34 ne {w} lt with zc11 ? ⟪ proj1 lt , ? ⟫
 ... | case1 lt = SUP.x<sup zc32 lt
 ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
 zc33 : supf0 z ≡ & (SUP.sup zc32)
-zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
+zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
 zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
-zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  }
+zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  }
 zc35 : STMP z≤x
 zc35 with trio< (supf0 px) px
 ... | tri< a ¬b ¬c = zc36 ¬b
 ... | tri> ¬a ¬b c = zc36 ¬b
-... | tri≈ ¬a b ¬c = record { tsup = zc37 ; tsup=sup = ?  } where
+... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
-zc37 : SUP A (UnionCF A f mf ay supf0 z)
+zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
-zc37 = record { sup = ? ; as = ? ; x<sup = ? }
+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≤-refl0 b) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))
 sis {z} z≤x with trio< z x
 ... | tri< a ¬b ¬c = {!!} where
-zc8 = ZChain.supf-is-sup (pzc z a) {!!}
+zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
 sup=u {z} ab z≤x is-sup with trio< z x
 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }

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

comparison src/zorn.agda @ 891:9fb948dac666