diff Ordinals.agda @ 339:feb0fcc430a9

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Jul 2020 19:55:37 +0900
parents bca043423554
children 639fbb6284d8
line wrap: on
line diff
--- a/Ordinals.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/Ordinals.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -21,7 +21,8 @@
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      not-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
-     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y )
+     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y ) ∧
+        ( (x : ord) → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)  ))
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -219,6 +220,14 @@
           → ¬ p
         FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+        next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+        next< {x} {y} {z} x<nz y<nx with trio< y (next z)
+        next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
+        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) (next z) x<nz (subst (λ k → k o< next x) b y<nx)
+           (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (proj1 (proj2 next-limit) w (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
+        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx )
+           (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal