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

changeset 839:710574600659

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, 28 Aug 2022 14:46:18 +0900
parents 1a5bb940fceb
children 52bff0b4cb37
files src/zorn.agda
diffstat 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Aug 28 09:15:52 2022 +0900
+++ b/src/zorn.agda	Sun Aug 28 14:46:18 2022 +0900
@@ -755,7 +755,11 @@
                           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₁) ⟫ 
-                          zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu  , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) ? (init ? ? ) ⟫ 
+                          zc12 (init asu su=z ) with trio< u px
+                          ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu  , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) 
+                              record { fcy<sup = ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫ 
+                          ... | tri≈ ¬a b ¬c = ?
+                          ... | tri> ¬a ¬b c = ?
                      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