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

comparison src/zorn.agda @ 938:93a49ffa9183

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 28 Oct 2022 18:37:05 +0900
parents	3a511519bd10
children	187594116449

comparison

equal deleted inserted replaced

-:3a511519bd10
+:93a49ffa9183
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
 ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca
+ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca
 ... | case1 eq with s≤fc (supf ub) f mf fcb
 ... | 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
 ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
 ct01 : * a < * b
 ct01 = subst (λ k → * k < * b ) (sym eq) lt
-ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
 ct00 : * a < * (supf ub)
 ct00 = lt
 ct01 : * a < * b
 ct01 with s≤fc (supf ub) f mf fcb
 ... | case1 eq =  subst (λ k → * a < k ) eq ct00
 ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
+ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
 ... | case1 eq with s≤fc (supf ua) f mf fca
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * a ≡ * b
 ct00 = sym (trans (cong (*) eq) eq1 )
 ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
 ct01 : * b < * a
 ct01 = subst (λ k → * k < * a ) (sym eq) lt
-ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
 ct00 : * b < * (supf ua)
 ct00 = lt
 ct01 : * b < * a
 ct01 with s≤fc (supf ua) f mf fca
 ... | case1 eq =  subst (λ k → * b < k ) eq ct00
 chain∋init : odef chain y
 chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
 f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a)
 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-f-next {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 ) ⟫
+f-next {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 ) ⟫
 initial : {z : Ordinal } → odef chain z → * y ≤ * z
 initial {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
+... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
 zc7 : y <= supf u
 zc7 = ChainP.fcy<sup is-sup (init ay refl)
 f-total : IsTotalOrderSet chain
 f-total {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) )
 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (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 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 , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
+... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
-(sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫
+(sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
 supf = ZChain.supf zc
 csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
 csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
 zc05 with zc04
 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
-... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where
+... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where
 zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
 zc07 = fc
 zc06 : supf u ≡ u
 zc06 = ChainP.supu=u is-sup
 zc08 : supf u o< supf b
 zc08 = ordtrans≤-< (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc ))) ss<sb
 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
 zc04 : odef (UnionCF A f mf ay supf b) (f x)
 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) ⟫
+... | ⟪ 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  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
 zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc ))
 -- supf (supf b) ≡ supf b
 u<x :  u o< x
 u<x = ?
 zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) 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₁) ⟫
+... | ⟪ 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 trio< u px | inspect supf1 u
 ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u
 ?
 record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) } zc14 ⟫  where
 zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ?  ⟫ )
 zc12 {z} (case2 fc) = zc21 fc where
 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₁) ⟫
+... | ⟪ 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 )
 ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px ? -- (pxo<x op)
 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
 zc15 : supf1 px ≡ px
 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
 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 ?
 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 )
 z11 {s} {z} lt fc  = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? ))
 (ChainP.order is-sup lt0 (fcup fc s≤px )) where
 s<u : s o< u
 s<u = supf-inject0 supf1-mono lt
 s≤px : s o≤ px
-s≤px = ordtrans s<u ? -- (o<→≤ u≤x)
+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)
 s1u=x = trans ? eq
 zc13 : osuc px o< osuc u1
 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) )
 x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
 x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
-x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? ))
+x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? ))
 ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where
 zc14 : u ≡ osuc px
 zc14 = begin
 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩
 supf0 u ≡⟨ ? ⟩
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay supf x) b f →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max-hp supf 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 ,
+... | ⟪ 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))  ⟫
+--     (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
 zc70 : HasPrev A pchain x f → ¬ xSUP pchain x
 zc70 pr xsup = ?
 no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
 pchain0=1 : pchain ≡ pchain1
 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc10 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc12 fc where
+zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where
 zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
 zc12 (fsuc x fc) with zc12 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₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
 zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫
 zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where
+zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where
 zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
 zc13 (fsuc x fc) with zc13 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₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
 zc13 (init asu su=z ) with trio< u x
 ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫
 ... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u≤x c )
+... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c )
 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
 sup {z} z≤x with trio< z x
 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
 sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
 → supf mc << MinSUP.sup spd
 sc<<d {mc} {asc} spd = z25 where
 d1 :  Ordinal
-d1 = MinSUP.sup spd
+d1 = MinSUP.sup spd -- supf d1 ≡ d
 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
 z24 = MinSUP.x<sup spd (init asc refl)
-z26 :  odef (ZChain.chain zc) (supf mc)
-z26 = ?
 z28 : supf mc o< & A
 z28 = z09 (ZChain.asupf zc)
 z25 : supf mc << d1
 z25 with z24
 ... | case2 lt = lt
-... | case1 eq = ? where
+... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
+--  supf mc ≡ d1
 z27 :  odef (ZChain.chain zc) (cf nmx d1)
 z27 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k ) eq (ZChain.csupf zc z28))
+z31 : {z w : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z
+→ (* w ≡ * z) ∨ (* w < * z)
+→ (* w ≡ * d1) ∨ (* w < * d1)
+z31 {z} uz (case1 w=z) with MinSUP.x<sup spd uz
+... | case1 eq = case1 (trans w=z (cong (*) eq) )
+... | case2 lt = case2 (subst (λ k → k < * d1 ) (sym w=z) lt )
+z31 {z} {w} uz (case2 w<z) with MinSUP.x<sup spd uz
+... | case1 eq = case2 (subst (λ k → * w < k ) (cong (*) eq) w<z )
+... | case2 lt = case2 (  IsStrictPartialOrder.trans PO w<z lt)
+z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+z29 with z27
+... | ⟪ aa , ch-init fc ⟫ = ? where
+z30 : FClosure A (cf nmx) (& s) (cf nmx d1)
+z30 = fc
+... | ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ with trio< u (supf mc) -- u<x : supf u o< supf (& A)
+... | tri< a ¬b ¬c = ?  -- u o< supf mc
+... | tri> ¬a ¬b c = ?  -- supf mc o< u
+... | tri≈ ¬a b ¬c with MinSUP.x<sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup) b) refl fc )
+... | case1 eq = case1 (cong (*) eq)
+... | case2 lt = case2 lt
 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
 ... | case2 lt = lt

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

comparison src/zorn.agda @ 938:93a49ffa9183