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

comparison src/zorn.agda @ 833:3fa321cbc337

... dead end

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 23 Aug 2022 10:33:47 +0900
parents	e61cbf28ec31
children	6bf0899a6150

comparison

equal deleted inserted replaced

-:e61cbf28ec31
+:3fa321cbc337
 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay)
 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
 SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
+record xSUP (B : HOD) (x : Ordinal) : Set n where
+field
+ax : odef A x
+is-sup : IsSup A B ax
 --
 -- create all ZChains under o< x
 --
 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
 pcy : odef pchain y
 pcy = ⟪ ay , ch-init (init ay refl)    ⟫
 supf0 = ZChain.supf zc
-sup1 : SUP A (UnionCF A f mf ay supf0 px)
-sup1 = supP pchain pchain⊆A ptotal
-sp1 = & (SUP.sup sup1 )
-supf1 : Ordinal → Ordinal
-supf1 z with trio< z px
-... | tri< a ¬b ¬c = ZChain.supf zc z
-... | tri≈ ¬a b ¬c = sp1
-... | tri> ¬a ¬b c = sp1
-pchain1 : HOD
-pchain1  = UnionCF A f mf ay supf1 x
-pcy1 : odef pchain1 y
-pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
-pinit1 :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
-pinit1 {a} ⟪ aa , ua ⟫  with  ua
-... | ch-init fc = s≤fc y f mf fc
-... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-zc7 : y <= supf1 u
-zc7 = ChainP.fcy<sup is-sup (init ay refl)
-pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
-pnext1 {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
-ptotal1 : IsTotalOrderSet pchain1
-ptotal1 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
-zc64 : {z : Ordinal } → supf0 z o< supf0 px → odef (UnionCF A f mf ay supf0 px) (supf0 z)
-zc64 {z} sz<spx = zc73 where
-z<px = ZChain.supf-inject zc sz<spx
-zc70 : odef (UnionCF A f mf ay supf0 (supf0 z) ) (supf0 z)
-zc70 = ZChain.csupf zc (o<→≤ z<px )
-zc73 : odef (UnionCF A f mf ay supf0 px ) (supf0 z)
-zc73 with osuc-≡< (ZChain.supf-mono zc (o<→≤ z<px))
-... | case1 eq2 = ⊥-elim ( o<¬≡ eq2 sz<spx )
-... | case2 lt = subst (λ k → odef (UnionCF A f mf ay supf0 px ) k ) &iso ( ZChain.csupf-fc zc  o≤-refl lt (init (proj1 zc70) refl) )
-supf1<sp1 : {z : Ordinal } → supf1 z o≤ sp1
-supf1<sp1 {z} = ? where
-zc50 : supf0 px ≡ sp1
-zc50 = ? -- ZChain.sup=u zc ? ? ?
-zc53 : SUP A ( UnionCF A f mf ay supf0 px )
-zc53 = ZChain.sup zc o≤-refl
-zc52 : supf0 px ≡ ?
-zc52 = ? -- ZChain.sup=u zc ? ? ?
-zc51 : supf0 sp1 ≡ sp1
-zc51 = ZChain.sup=u zc ? ? ?
 -- if previous chain satisfies maximality, we caan reuse it
 --
 --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
-record xSUP : Set n where
+no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x
-field
+no-extension ¬sp=x = record { supf = supf0 ;  sup = ? ; supf-mono = {!!}
-ax : odef A x
+; initial = ? ; chain∋init = ? ; sup=u = ? ; supf-is-sup = ? ; csupf = {!!}
-is-sup : IsSup A (UnionCF A f mf ay supf0 px) ax
+;  chain⊆A = λ lt → proj1 lt ;  f-next = ? ;  f-total = ? }  where
+pchain0=1 : ?
-UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o< px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1
+pchain0=1 = ?
-UnionCF⊆ {z0} {z1} z0≤1 z0<px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
+sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf0 z)
-UnionCF⊆ {z0} {z1} z0≤1 z0<px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
-zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w
-zc60 (init asp refl) with trio< u1 px | inspect supf1 u1
-... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
-record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
-fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
-order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
-(z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-order {s} {z2} s<u1 fc with trio< s px
-... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup zc61 fc ) where
-zc61 : supf0 s o< supf0 u1
-zc61 = subst (λ k → supf0 s o< k ) eq1 s<u1
-... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> supf1<sp1 s<u1 )
-... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s {!!} ))  --  px o< s < u1 < px
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
-record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 {!!}   } (init (subst (λ k → odef A k ) (sym eq1) {!!} ) {!!} )  ⟫ where
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
-fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) {!!} -- ( ChainP.fcy<sup u1-is-sup fc )
-order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
-(z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-order {s} {z2} s<u1 fc with trio< s px
-... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) {!!}
-... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) {!!} -- ( ChainP.order u1-is-sup s<u1 fc )
-... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b {!!} ) ))  --  px o< s < u1 = px
-... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x (o<→≤ z0<px))
-... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 )
-... | case2 lt = ⊥-elim ( o<> lt px<u1 )
-zc60 (fsuc w1 fc) with zc60 fc
-... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
-no-extension : ¬ xSUP → ZChain A f mf ay x
-no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = {!!}
-; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = {!!}
-;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
-UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o< x → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1
-UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
-UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
-zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w
-zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1
-... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
-record { fcy<sup = fcy<sup ; order = {!!} ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init asp refl )  ⟫ where
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
-fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
-order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
-(z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
-order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) {!!} ))
-... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
-record { fcy<sup = fcy<sup ; order = {!!} ; supu=u = trans (sym {!!} ) (ChainP.supu=u u1-is-sup)   } (init {!!} {!!} )  ⟫ where
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
-fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) {!!} ( ChainP.fcy<sup u1-is-sup fc )
-order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
-(z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
-order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) {!!}( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) {!!} ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) {!!} ))
-... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
-... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px
-... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) )
-... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 )
-... | case2 lt = ⊥-elim ( o<> lt px<u1 )
-zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq1} | tri≈ ¬a' b ¬c with osuc-≡< (OrdTrans u1≤x (o≤-refl0 b) )
-... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 )
-... | case2 lt = ⊥-elim ( o<> lt px<u1 )
-zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq1} | tri> ¬a' ¬b' px<z0 = ⊥-elim (¬p<x<op ⟪ px<z0 , subst (λ k → z0 o< k ) (sym (Oprev.oprev=x op)) z0<x  ⟫ )
-zc60 (fsuc w1 fc) with zc60 fc
-... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
-sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
 sup {z} z≤x with trio< z px
-... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ?  ) ( ZChain.sup zc (o<→≤   a) )
+... | tri< a ¬b ¬c = SUP⊆ ? ( ZChain.sup zc (o<→≤   a) )
-... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
+... | tri≈ ¬a b ¬c = record { sup = SUP.sup ? ; as = SUP.as ? ; x<sup = ? } where
-zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
+zc61 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup ?) ∨ (w < SUP.sup ? )
 zc61 {w} lt = ? -- SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x  lt )
 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) ? ⟫ )
 sup=u : {b : Ordinal} (ab : odef A b) →
-b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
+b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab → 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 is-sup (UnionCF⊆ o≤-refl  a lt) }
+... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup ? }
 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) }
-... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
+... | tri> ¬a ¬b px<b = ? where -- ⊥-elim (¬sp=x zcsup ) 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
+zcsup : ?
-zcsup with zc30
+zcsup = ? -- with zc30
-... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) {!!} lt) } }
+-- ... | refl = case1 record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup ? } }
-csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
+csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 b) (supf0 b)
-csupf {b} b<x with trio< b px | inspect supf1 b
+csupf {b} b<x with trio< b px | inspect supf0 b
-... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a {!!}
+... | tri< a ¬b ¬c | _ = ? -- UnionCF⊆ o≤-refl a {!!}
 ... | tri≈ ¬a refl ¬c | _ = {!!} -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = {!!} --  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl )
-sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
+sis : {z : Ordinal} (z≤x : z o≤ x) → supf0 z ≡ & (SUP.sup (sup z≤x))
 sis {z} z<x with trio< z px
 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc (o<→≤ a )
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) ?  ⟫ )
 zc4 : ZChain A f mf ay x
 zc4 with ODC.∋-p O A (* x)
 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )
 -- we have to check adding x preserve is-max ZChain A y f mf x
 ... | no lim = zc5 where
 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
 pzc z z<x = prev z z<x
-ysp =  & (SUP.sup (ysup f mf ay))
+record Usupf : Set n where
-record SupE ( z : Ordinal ) : Set n where
 field
-z<x : z o< x
+umax : Ordinal → Ordinal
-z=supfz : z ≡  ZChain.supf (pzc z z<x) z
+umax<x : {z : Ordinal } → umax z o< x
+supf : Ordinal → Ordinal
-psupf0 : (z : Ordinal) → Ordinal
+supf z = ZChain.supf (pzc (osuc (umax z)) (ob<x lim umax<x )) z
-psupf0 z with trio< z x
+field
-... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
-... | tri≈ ¬a b ¬c = ysp
-... | tri> ¬a ¬b c = ysp
-pchain0 : HOD
-pchain0 = UnionCF A f mf ay psupf0 x
-ptotal0 : IsTotalOrderSet pchain0
-ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-uz01 = chain-total A f mf ay psupf0 ( (proj2 ca)) ( (proj2 cb))
-usup : SUP A pchain0
-usup = supP pchain0 (λ lt → proj1 lt) ptotal0
-spu = & (SUP.sup usup)
 supf1 : Ordinal → Ordinal
-supf1 z with trio< z x
+supf1 z = ?
-... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+-- ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-... | tri≈ ¬a b ¬c = spu
-... | tri> ¬a ¬b c = spu
 pchain : HOD
 pchain = UnionCF A f mf ay supf1 x
 pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
 ... | ⟪ 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 ,
 subst (λ k → UChain A f mf ay supf x k )
 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫
-record xSUP : Set n where
+no-extension : ¬ ( xSUP (UnionCF A f mf ay supf1 x) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x
-field
-ax : odef A x
-not-sup : IsSup A (UnionCF A f mf ay psupf0 x) ax
-no-extension : ¬ xSUP → ZChain A f mf ay x
 no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
 ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!}
 ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫
 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = {!!} -- with
 --                      UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫
 --                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
 --                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-UnionCFR⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay psupf0 x
+UnionCFR⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf1 x
 UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫
 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = {!!} -- with
 --                      UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫
 --                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
 zc8 = ZChain.supf-is-sup (pzc z a) {!!}
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b c = {!!}
 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
 sup=u {b} ab b<x is-sup with trio< b x
-... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
+... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }
 ... | tri> ¬a ¬b c = {!!}
 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
 csupf {z} z≤x with trio< z x
-... | tri< a ¬b ¬c = zc9 where
+... | tri< a ¬b ¬c = ?  where
 zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
 zc9 = {!!}
 zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
 zc8 = {!!} -- ZChain.csupf  (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc )
 ... | tri≈ ¬a b ¬c = {!!}

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

comparison src/zorn.agda @ 833:3fa321cbc337