Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1481:42df464988e8
o<-irr reintroduce
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 30 Jun 2024 13:05:00 +0900 |
| parents | ba406e2ba8af |
| children | 4f597bc6b3d6 |
| files | src/Ordinals.agda src/ordinal.agda src/zorn.agda |
| diffstat | 3 files changed, 8 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Ordinals.agda Sun Jun 30 11:03:33 2024 +0900 +++ b/src/Ordinals.agda Sun Jun 30 13:05:00 2024 +0900 @@ -26,7 +26,7 @@ <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x ) - -- o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1 + o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1 TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x
--- a/src/ordinal.agda Sun Jun 30 11:03:33 2024 +0900 +++ b/src/ordinal.agda Sun Jun 30 13:05:00 2024 +0900 @@ -225,6 +225,7 @@ ; osuc-≡< = osuc-≡< ; TransFinite = TransFinite2 ; Oprev-p = Oprev-p + ; o<-irr = OrdIrr _ _ } -- -- isNext = record { -- x<nx = x<nx
--- a/src/zorn.agda Sun Jun 30 11:03:33 2024 +0900 +++ b/src/zorn.agda Sun Jun 30 13:05:00 2024 +0900 @@ -1224,7 +1224,8 @@ fc12 = ftrans<-≤ lt (subst (λ k → k ≤ a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca ) ) pcmp (ic-isup i i<x s<x fca) (ic-isup i i<y s<y fcb) refl = fcn-cmp _ f mf fca (subst (λ k → FClosure A f k b) pc01 fcb ) where pc01 : supfz i<y ≡ supfz i<x - pc01 = zeq ? ? ? ? + pc01 = cong supfz o<-irr + -- zeq does not work here ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) ib<ia) @@ -1385,16 +1386,16 @@ sa = ZChain.supf (pzc (ob<x lim a<x)) a m = omax a sa -- x is limit ordinal, so we have sa o< m o< x m<x : m o< x - m<x with trio< a sa | inspect (omax a) sa - ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim (ordtrans<-≤ sa<b b≤x ) - ... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where + m<x with trio< a sa + ... | tri< a<sa ¬b ¬c = ob<x lim (ordtrans<-≤ sa<b b≤x ) + ... | tri≈ ¬a a=sa ¬c = subst (λ k → k o< x) ? zc41 where zc41 : omax a sa o< x zc41 = osucprev ( begin osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩ osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩ osuc ( osuc a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x)) ⟩ x ∎ ) where open o≤-Reasoning O - ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x + ... | tri> ¬a ¬b c = ob<x lim a<x sam = ZChain.supf (pzc (ob<x lim m<x)) a zc42 : osuc a o≤ osuc m zc42 = osucc (o<→≤ ( omax-x _ _ ) )