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

comparison src/zorn.agda @ 1032:382680c3e9be

minsup is not obvious in ZChain

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 30 Nov 2022 20:43:01 +0900
parents	f276cf614fc5
children	2da8dcbb0825

comparison

equal deleted inserted replaced

-:f276cf614fc5
+:382680c3e9be
 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
 (IsStrictPartialOrder.trans PO     b<a a<b)
+<<-irr : {a b : Ordinal } → a ≤ b  → b << a → ⊥
+<<-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (cong (*) (sym a=b)) b<a
+<<-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO refl (IsStrictPartialOrder.trans PO b<a a<b)
 ptrans =  IsStrictPartialOrder.trans PO
 open _==_
 open _⊆_
 _⊆'_ : ( A B : HOD ) → Set n
 _⊆'_ A B = {x : Ordinal } → odef A x → odef B x
 --
--- inductive maxmum tree from x
+-- inductive masum tree from x
 -- tree structure
 --
 record HasPrev (A B : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal )   : Set n where
 field
 fc-total : (A : HOD ) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (supf : Ordinal → Ordinal )
 (order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y)
 {s s1 a b : Ordinal } ( fa : FClosure A f (supf s) a )( fb : FClosure A f (supf s1) b )  → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 fc-total A f mf supf order {xa} {xb} {a} {b} ca cb with trio< xa xb
-... | tri< a₁ ¬b ¬c with order a₁ ca
+... | tri< a₁ ¬b ¬c with ≤-ftrans  (order a₁ ca ) (s≤fc (supf xb) f mf cb )
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * a ≡ * b
-ct00 = ? -- trans (cong (*) eq) eq1
+ct00 = cong (*) eq1
-... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
-ct02 : * a < * b
+fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri≈ _ refl _ = fcn-cmp _ f mf ca cb
-ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt
+fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri> ¬a ¬b c with ≤-ftrans  (order c cb ) (s≤fc (supf xa) f mf ca )
-fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri≈ a₁ ¬b ¬c = ?
+... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri> ¬a ¬b c = ?
+ct00 : * a ≡ * b
+ct00 = cong (*) (sym eq1)
+... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 record IsMinSUP ( A B : HOD ) (sup : Ordinal) : Set n where
 field
-axm : odef A sup
+as : odef A sup
 x≤sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup )
 minsup : { sup1 : Ordinal } → odef A sup1
 →  ( {x : Ordinal  } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 ))  → sup o≤ sup1
 record MinSUP ( A B : HOD )  : Set n where
 field
 sup : Ordinal
 isMinSUP : IsMinSUP A B sup
-axm = IsMinSUP.axm isMinSUP
+as = IsMinSUP.as isMinSUP
 x≤sup = IsMinSUP.x≤sup isMinSUP
 minsup = IsMinSUP.minsup isMinSUP
 z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
 z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 M→S  : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} {y : Ordinal} {ay : odef A y}  { x : Ordinal }
 →  (supf : Ordinal → Ordinal )
 →  MinSUP A (UnionCF A f supf x)
 → SUP A (UnionCF A f supf x)
 M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms)
-; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.axm ms) ; x≤sup = ? } } where
+; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.as ms) ; x≤sup = ms00 } } where
-msup = MinSUP.sup ms
+ms00 :  {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ & (* (MinSUP.sup ms))) ∨ (z << & (* (MinSUP.sup ms)))
-ms00 : {z : HOD} → UnionCF A f supf x ∋ z → (z ≡ * msup) ∨ (z < * msup)
 ms00 {z} uz with MinSUP.x≤sup ms uz
-... | case1 eq = case1 (subst (λ k → k ≡ _) *iso ( cong (*) eq))
+... | case1 eq = case1 (subst (λ k → z ≡ k) (sym &iso) eq)
-... | case2 lt = case2 (subst₂ (λ j k →  j < k ) *iso refl lt )
+... | case2 lt = case2  (subst (λ k →  * z < k ) (sym *iso) lt )
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
 (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
 → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫
-chain-minsup : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )    (supf : Ordinal → Ordinal )
-( order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y)
-{x : Ordinal} → IsMinSUP A (UnionCF A f supf x) x
-chain-minsup = ?
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
 field
 supf :  Ordinal → Ordinal
-sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-→ IsSUP A (UnionCF A f supf b) b ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b
 cfcs : (mf< : <-monotonic-f A f)
 {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f supf b) w
+fcy<sup  : {w : Ordinal } → FClosure A f y w → (w ≡ supf o∅  ) ∨ ( w << supf o∅  )
 order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
-supf0 : supf o∅ ≡ y
+is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f supf x) (supf x)
-minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
+sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
+→ IsSUP A (UnionCF A f supf b) b ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b
 chain : HOD
 chain = UnionCF A f supf z
 chain⊆A : chain ⊆' A
 chain⊆A = λ lt → proj1 lt
-sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f supf x)
-sup {x} x≤z = M→S supf (minsup x≤z)
-s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z)
-s=ms {x} x≤z = &iso
 chain∋init : odef chain y
 chain∋init = ⟪ ay , ?   ⟫
 f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a)
 f-next {a} ⟪ aa , cp  ⟫ = ?
 initial : {z : Ordinal } → odef chain z →  y ≤  z
 initial {a} ⟪ aa , ua ⟫  = ?
 f-total : IsTotalOrderSet chain
-f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
+f-total {a} {b} ca cb = ?
-uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+-- subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-uz01 = ? -- chain-total A f supf ( (proj2 ca)) ( (proj2 cb))
+--     uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+--    uz01 with trio< (& a) (& b)
+--    ... | tri> ¬a ¬b c = ?
+--   ... | tri≈ ¬a b ¬c = ?
+--  ... | tri< a ¬b ¬c = ?
 supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
 supf-inject {x} {y} sx<sy with trio< x y
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
 csupf : (mf< : <-monotonic-f A f) {b : Ordinal }
 → supf b o< supf z → supf b o< z → odef (UnionCF A f supf z) (supf b) -- supf z is not an element of this chain
 csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
-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
+minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
-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) , ? ⟫
+minsup {x} x≤z = record { sup = supf x ; isMinSUP = is-minsup x≤z }
-... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
-... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
+supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup (minsup x≤z)
+supf-is-minsup _ = refl
--- ordering is not proved here but in ZChain1
+chain-minsup : {x : Ordinal} → IsMinSUP A (UnionCF A f supf x) (supf x)
+chain-minsup {x} = record { as = as ; x≤sup = cp1 ; minsup = cpm } where
+as : odef A (supf x)
+as = asupf
+cp1 : {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ supf x) ∨ (z << supf x)
+cp1 {z} ⟪ az , ch-is-sup u u<x supu=u fc ⟫ = order u<x fc
+cpm :  {s : Ordinal} → odef A s → ({z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ s) ∨ (z << s)) → supf x o≤ s
+cpm {s} as z≤s with trio< (supf x) s
+... | tri< a ¬b ¬c = o<→≤ a
+... | tri≈ ¬a b ¬c = o≤-refl0 b
+... | tri> ¬a ¬b c = ? where
+cp4 : supf (supf s) ≡ supf s
+cp4 = ?
+cp3 : supf s o< x
+cp3 = ?
+cp2 : odef (UnionCF A f supf x) (supf s)
+cp2 =  ⟪ asupf , ch-is-sup (supf s) cp3 cp4 (init asupf cp4)  ⟫
+--        ... | case1 eq = ?
+--        ... | case2 lt = ?
 IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
 → ({y : Ordinal} → odef (UnionCF A f supf x) y → (y ≡ sp ) ∨ (y << sp ))
 → ( {a : Ordinal } → odef A a → a << f a )
 → ¬ ( HasPrev A (UnionCF A f supf x) f sp )
-IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr  ? sp<fsp ) where
+IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<<-irr fsp≤sp sp<fsp ) where
 sp<fsp : sp << f sp
 sp<fsp = <-mono-f asp
 pr = HasPrev.y hp
 im00 : f (f pr) ≤ sp
 im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
 sxa=sxb with trio< (supfa x) (supfb x)
 ... | tri≈ ¬a b ¬c = b
 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (
 begin
 supfb x  ≡⟨ sbx=spb ⟩
-spb  ≤⟨ MinSUP.minsup mb (MinSUP.axm ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
+spb  ≤⟨ MinSUP.minsup mb (MinSUP.as ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
 spa ≡⟨ sym sax=spa ⟩
 supfa x ∎ ) a ) where
 open o≤-Reasoning O
 z53 : {z : Ordinal } →  odef (UnionCF A f (ZChain.supf zb) x) z →  odef (UnionCF A f (ZChain.supf za) x) z
 z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
 begin
 supfa x  ≡⟨ sax=spa ⟩
-spa  ≤⟨ MinSUP.minsup ma (MinSUP.axm mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
+spa  ≤⟨ MinSUP.minsup ma (MinSUP.as mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
 spb  ≡⟨ sym sbx=spb ⟩
 supfb x ∎ ) c ) where
 open o≤-Reasoning O
 z53 : {z : Ordinal } →  odef (UnionCF A f (ZChain.supf za) x) z →  odef (UnionCF A f (ZChain.supf zb) x) z
 z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫
 ... | tri≈ ¬a b ¬c = case1 ( λ lt →  ⊥-elim ( ¬a lt )  )
 ... | tri> ¬a ¬b c = case1 ( λ lt →  ⊥-elim ( ¬a lt )  )
 ... | tri< a ¬b ¬c with prev z a
 ... | case2 mins = case2 mins
 ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z)
-... | case1 mins = case2 record { sup = z ; isMinSUP = record { axm = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where
+... | case1 mins = case2 record { sup = z ; isMinSUP = record { as = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where
 m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1
 m04 {s} as lt with trio< z s
 ... | tri< a ¬b ¬c = o<→≤ a
 ... | tri≈ ¬a b ¬c = o≤-refl0 b
 ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫  )
 asupf1 : {z : Ordinal } → odef A (supf1 z)
 asupf1 {z} with trio< z px
 ... | tri< a ¬b ¬c = ZChain.asupf zc
 ... | tri≈ ¬a b ¬c = ZChain.asupf zc
-... | tri> ¬a ¬b c = MinSUP.axm sup1
+... | tri> ¬a ¬b c = MinSUP.as sup1
 supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
 supf1-mono {a} {b} a≤b with trio< b px
 ... | tri< a ¬b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ (ordtrans≤-< a≤b a)))) refl ( supf-mono a≤b )
 ... | tri≈ ¬a b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (subst (λ k → a o≤ k) b a≤b))) refl ( supf-mono a≤b )
 zc21 : MinSUP A (UnionCF A f supf0 a)
 zc21 = ZChain.minsup zc (o<→≤ a<px)
 zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
 zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) )
 zc19 : supf0 a o≤ sp1
-zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.axm sup1) zc24 )
+zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
 ... | tri≈ ¬a b ¬c = zc18 where
 zc21 : MinSUP A (UnionCF A f supf0 a)
 zc21 = ZChain.minsup zc (o≤-refl0 b)
 zc20 : MinSUP.sup zc21 ≡ supf0 a
 zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b))
 zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
 zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
 zc18 : supf0 a o≤ sp1
-zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.axm sup1) zc24 )
+zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
 ... | tri> ¬a ¬b c = o≤-refl
 sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
 sf≤ {z} x≤z with trio< z px
 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
 tsup : MinSUP A (UnionCF A f supf1 z)
 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 = record { sup = MinSUP.sup m  ; asm = MinSUP.axm m
+... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
 m = ZChain.minsup zc (o<→≤ a)
 ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
 ms00 {w} ⟪ az , cp ⟫ = MinSUP.x≤sup m ⟪ az , ? ⟫
 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
 odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
 ms01 {sup2} us P = MinSUP.minsup m us ?
-... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.axm m
+... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
 m = ZChain.minsup zc (o≤-refl0 b)
 ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
 ms00 {x} ux = MinSUP.x≤sup m ?
 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
 odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
 ms01 {sup2} us P = MinSUP.minsup m us ?
-... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.axm sup1
+... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.as sup1
 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
 m = sup1
 ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
 ms00 {x} ux = MinSUP.x≤sup m ?
 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
 ... | 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 ⟫ )
-zc32 = ZChain.sup zc o≤-refl
+zc32 = ?
 zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
 zc34 ne {w} lt = ?
 zc33 : supf0 z ≡ & (SUP.sup zc32)
 zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
 zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
 chain = ZChain.chain zc
 supf = ZChain.supf zc
 sp : Ordinal
 sp = MinSUP.sup sp1
 asp : odef A sp
-asp = MinSUP.axm sp1
+asp = MinSUP.as sp1
 z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
 →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f (ZChain.supf zc) b) b
 → * a < * b  → odef chain b
 z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
 z22 : sp o< & A
 ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p )
 z14 :  f sp ≡ sp
 z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 )
 ... | tri< a ¬b ¬c = ⊥-elim z16 where
 z16 : ⊥
-z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.axm sp1 ))
+z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.as sp1 ))
 ... | case1 eq = ⊥-elim (¬b (sym (cong (*) eq ) ))
 ... | case2 lt = ⊥-elim (¬c lt )
 ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b )
 ... | tri> ¬a ¬b c = ⊥-elim z17 where
 z15 : (f sp ≡ MinSUP.sup sp1) ∨ (* (f sp) < * (MinSUP.sup sp1) )
 -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
 --
 z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
 z04 nmx zc = <-irr0  {* (cf nmx c)} {* c}
-(subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.axm  msp1 ))))
+(subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
-(subst (λ k → odef A k) (sym &iso) (MinSUP.axm msp1) )
+(subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
-(proj1 (cf-is-<-monotonic nmx c (MinSUP.axm msp1 ))) where          -- x < f x
+(proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1 ))) where          -- x < f x
 supf = ZChain.supf zc
 msp1 : MinSUP A (ZChain.chain zc)
 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
 c : Ordinal

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

comparison src/zorn.agda @ 1032:382680c3e9be