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

comparison src/zorn.agda @ 663:5f85e71b2490

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 03 Jul 2022 17:08:55 +0900
parents a45ec34b9fa7
children 6a8d13b02a50
comparison
equal deleted inserted replaced
662:a45ec34b9fa7 663:5f85e71b2490
248 chain∋z : odef (chain u u<x) z 248 chain∋z : odef (chain u u<x) z
249 249
250 ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A 250 ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
251 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 251 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
252 252
253 UnionCF : (A : HOD) (x : Ordinal) (chainf : (z : Ordinal ) → z o< x → HOD ) → HOD
254 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
255
253 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) : Ordinal → HOD → Set (Level.suc n) where 256 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) : Ordinal → HOD → Set (Level.suc n) where
254 ch-noax : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f ay (Oprev.oprev op) chain) → Chain A f ay x chain 257 ch-noax : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f ay (Oprev.oprev op) chain) → Chain A f ay x chain
255 ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 258 ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x )
256 ( c : Chain A f ay (Oprev.oprev op) chain) ( h : HasPrev A chain ax f ) → Chain A f ay x chain 259 ( c : Chain A f ay (Oprev.oprev op) chain) ( h : HasPrev A chain ax f ) → Chain A f ay x chain
257 ch-is-sup : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 260 ch-is-sup : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x )
258 ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬ HasPrev A chain ax f ) ( sup : IsSup A chain ax ) → Chain A f ay x 261 ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬ HasPrev A chain ax f ) ( sup : IsSup A chain ax ) → Chain A f ay x
259 record { od = record { def = λ z → odef A z ∧ (odef chain z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 262 record { od = record { def = λ z → odef A z ∧ (odef chain z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
260 ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 263 ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x )
261 ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬ HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain 264 ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬ HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain
262 ch-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 265 ch-noax-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( noax : ¬ odef A x )
263 → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x )) 266 → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
267 → Chain A f ay x (UnionCF A x chainf )
268 ch-hasprev-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x )
269 → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
270 → ( h : HasPrev A (UnionCF A x chainf) ax f )
271 → Chain A f ay x (UnionCF A x chainf )
272 ch-is-sup-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x )
273 → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
274 → ( nh : ¬ HasPrev A (UnionCF A x chainf) ax f ) ( sup : IsSup A (UnionCF A x chainf) ax )
264 → Chain A f ay x 275 → Chain A f ay x
265 record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y z ) } 276 record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y x ) }
266 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 277 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
278 ch-skip-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x )
279 → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
280 → (nh : ¬ HasPrev A (UnionCF A x chainf) ax f ) (nsup : ¬ IsSup A (UnionCF A x chainf) ax )
281 → Chain A f ay x (UnionCF A x chainf)
267 282
268 ChainF : (A : HOD) → ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f ay (& A) chain → (x : Ordinal) → x o< & A → HOD 283 ChainF : (A : HOD) → ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f ay (& A) chain → (x : Ordinal) → x o< & A → HOD
269 ChainF A f {y} ay chain Ch x x<a = ? 284 ChainF A f {y} ay chain Ch x x<a = {!!}
270 285
271 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where 286 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
272 field 287 field
273 chain : HOD 288 chain : HOD
274 chain-uniq : Chain A f ay z chain 289 chain-uniq : Chain A f ay z chain
275 290
276 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init) (zc0 : ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where 291 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init) (zc0 : ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
277 chain : HOD 292 chain : HOD
278 chain = ? 293 chain = {!!}
279 field 294 field
280 chain⊆A : chain ⊆' A 295 chain⊆A : chain ⊆' A
281 chain∋init : odef chain init 296 chain∋init : odef chain init
282 initial : {y : Ordinal } → odef chain y → * init ≤ * y 297 initial : {y : Ordinal } → odef chain y → * init ≤ * y
283 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 298 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
438 record { y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = sc6 } } where 453 record { y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = sc6 } } where
439 sc6 : x ≡ f (HasPrev.y pr) 454 sc6 : x ≡ f (HasPrev.y pr)
440 sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso ( HasPrev.x=fy pr ) 455 sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso ( HasPrev.x=fy pr )
441 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax ) 456 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax )
442 ... | case1 is-sup = record { chain = schain ; chain-uniq = sc9 } where 457 ... | case1 is-sup = record { chain = schain ; chain-uniq = sc9 } where
443 -- A∋sc -- x is a sup of zc
444 sup0 : SUP A (ZChain1.chain sc )
445 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
446 x21 : {y : HOD} → (ZChain1.chain sc ) ∋ y → (y ≡ * x) ∨ (y < * x)
447 x21 {y} zy with IsSup.x<sup is-sup zy
448 ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) )
449 ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x )
450 sp : HOD
451 sp = SUP.sup sup0
452 schain : HOD 458 schain : HOD
453 schain = record { od = record { def = λ x → odef A x ∧ ( odef (ZChain1.chain sc ) x ∨ (FClosure A f (& sp) x)) } 459 schain = record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) }
454 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 460 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
455 sc8 : Chain A f ay ? ? 461 sc7 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
456 sc8 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) ? ? 462 sc7 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
457 sc9 : Chain A f ay x schain 463 sc9 : Chain A f ay x schain
458 sc9 = ? 464 sc9 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7
459 ... | case2 ¬x=sup = {!!} 465 record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) }
460 ... | no ¬ox = ? where 466 ... | case2 ¬x=sup = record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where
461 supf : (z : Ordinal) → z o< x → HOD 467 sc17 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
462 supf = ? 468 sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
463 sc5 : HOD 469 sc10 : ¬ IsSup A (chain sc) (subst (λ k → odef A k) &iso ax)
464 sc5 = record { od = record { def = λ z → odef A z ∧ (UChain x supf z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 470 sc10 not = ¬x=sup ( record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) } )
471 ... | no ¬ox = {!!} where
472 chainf : (z : Ordinal) → z o< x → HOD
473 chainf z z<x = ZChain1.chain ( prev z z<x )
474 sc4 : ZChain1 A f ay x
475 sc4 with ODC.∋-p O A (* x)
476 ... | no noax = record { chain = UnionCF A x chainf ; chain-uniq = ? } -- ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? }
477 ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )
478 ... | case1 pr = record { chain = UnionCF A x chainf ; chain-uniq = ? } -- ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? }
479 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
480 ... | case1 is-sup = ?
481 ... | case2 ¬x=sup = ?
465 482
466 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f ay (& A)) 483 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f ay (& A))
467 → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x 484 → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x
468 ind f mf {y} ay x zc0 prev with Oprev-p x 485 ind f mf {y} ay x zc0 prev with Oprev-p x
469 ... | yes op = zc4 where 486 ... | yes op = zc4 where
482 499
483 -- if previous chain satisfies maximality, we caan reuse it 500 -- if previous chain satisfies maximality, we caan reuse it
484 -- 501 --
485 no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → 502 no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
486 HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab → 503 HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab →
487 * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay ? x 504 * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay {!!} x
488 no-extenion is-max = record { chain⊆A = ? -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc) 505 no-extenion is-max = record { chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
489 ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc) 506 ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc)
490 ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) 507 ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc)
491 ; f-total = ? 508 ; f-total = {!!}
492 ; chain∋init = subst (λ k → odef k y ) {!!} (ZChain.chain∋init zc) 509 ; chain∋init = subst (λ k → odef k y ) {!!} (ZChain.chain∋init zc)
493 ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) → 510 ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
494 HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) {!!} is-max } where 511 HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) {!!} is-max } where
495 supf0 : Ordinal → HOD 512 supf0 : Ordinal → HOD
496 supf0 z with trio< z x 513 supf0 z with trio< z x
635 ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab p a<b 652 ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab p a<b
636 ... | case1 b=x with p 653 ... | case1 b=x with p
637 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } ) 654 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
638 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 655 ... | case2 b=sup = ⊥-elim ( ¬x=sup record {
639 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) 656 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } )
640 ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = ? 657 ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!}
641 ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where --- limit ordinal case 658 ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where --- limit ordinal case
642 supf : Ordinal → HOD 659 supf : Ordinal → HOD
643 supf x = ZChain1.chain zc0 660 supf x = ZChain1.chain zc0
644 uzc : {z : Ordinal} → (u : UChain x ? z) → ZChain A f ay zc0 (UChain.u u) 661 uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f ay zc0 (UChain.u u)
645 uzc {z} u = prev (UChain.u u) (UChain.u<x u) 662 uzc {z} u = prev (UChain.u u) (UChain.u<x u)
646 Uz : HOD 663 Uz : HOD
647 Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z ? x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = ? } 664 Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!} }
648 u-next : {z : Ordinal} → odef Uz z → odef Uz (f z) 665 u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
649 u-next {z} = ? 666 u-next {z} = {!!}
650 -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u) } 667 -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u) }
651 -- u-next {z} (case2 u) = case2 ( fsuc _ u ) 668 -- u-next {z} (case2 u) = case2 ( fsuc _ u )
652 u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z 669 u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z
653 u-initial {z} = ? 670 u-initial {z} = {!!}
654 -- (case1 u) = ZChain.initial ( uzc u ) (UChain.chain∋z u) 671 -- (case1 u) = ZChain.initial ( uzc u ) (UChain.chain∋z u)
655 -- u-initial {z} (case2 u) = s≤fc _ f mf u 672 -- u-initial {z} (case2 u) = s≤fc _ f mf u
656 u-chain∋init : odef Uz y 673 u-chain∋init : odef Uz y
657 u-chain∋init = ? -- case2 ( init ay ) 674 u-chain∋init = {!!} -- case2 ( init ay )
658 supf0 : Ordinal → HOD 675 supf0 : Ordinal → HOD
659 supf0 z with trio< z x 676 supf0 z with trio< z x
660 ... | tri< a ¬b ¬c = ZChain1.chain zc0 677 ... | tri< a ¬b ¬c = ZChain1.chain zc0
661 ... | tri≈ ¬a b ¬c = Uz 678 ... | tri≈ ¬a b ¬c = Uz
662 ... | tri> ¬a ¬b c = Uz 679 ... | tri> ¬a ¬b c = Uz
663 u-mono : {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w 680 u-mono : {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
664 u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x 681 u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
665 ... | s | t = ? 682 ... | s | t = {!!}
666 683
667 seq : Uz ≡ supf0 x 684 seq : Uz ≡ supf0 x
668 seq with trio< x x 685 seq with trio< x x
669 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) 686 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
670 ... | tri≈ ¬a b ¬c = refl 687 ... | tri≈ ¬a b ¬c = refl
671 ... | tri> ¬a ¬b c = refl 688 ... | tri> ¬a ¬b c = refl
672 seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.chain zc0 ≡ supf0 b 689 seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.chain zc0 ≡ supf0 b
673 seq<x {b} b<x with trio< b x 690 seq<x {b} b<x with trio< b x
674 ... | tri< a ¬b ¬c = ? -- cong (λ k → (ZChain1.chain zc0) o<-irr -- b<x ≡ a 691 ... | tri< a ¬b ¬c = {!!} -- cong (λ k → (ZChain1.chain zc0) o<-irr -- b<x ≡ a
675 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) 692 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x )
676 ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) 693 ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x )
677 ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y 694 ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
678 ord≤< {x} {y} {z} x<z z≤y with osuc-≡< z≤y 695 ord≤< {x} {y} {z} x<z z≤y with osuc-≡< z≤y
679 ... | case1 z=y = subst (λ k → x o< k ) z=y x<z 696 ... | case1 z=y = subst (λ k → x o< k ) z=y x<z