Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 393:43b0a6ca7602
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 26 Jul 2020 21:10:37 +0900 |
| parents | 19687f3304c9 |
| children | 77c6123f49ee |
line wrap: on
line diff
--- a/OD.agda Sat Jul 25 17:36:27 2020 +0900 +++ b/OD.agda Sun Jul 26 21:10:37 2020 +0900 @@ -238,6 +238,12 @@ lemma {z} (case1 refl) = case1 refl lemma {z} (case2 refl) = case1 refl +pair-<xy : {x y : HOD} → {n : Ordinal} → od→ord x o< next n → od→ord y o< next n → od→ord (x , y) o< next n +pair-<xy {x} {y} {o} x<nn y<nn with trio< (od→ord x) (od→ord y) | inspect (omax (od→ord x)) (od→ord y) +... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< +... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< +... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< + -- another form of infinite -- pair-ord< : {x : Ordinal } → Set n pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x) @@ -427,8 +433,8 @@ lemma {o∅} iφ = x<nx lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) -ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ -ω<next-o∅ ho< {y} lt = <odmax infinite lt +ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ +ω<next-o∅ {y} lt = <odmax infinite lt nat→ω : Nat → HOD nat→ω Zero = od∅