# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661221555 -32400
# Node ID 6bf0899a6150a34a1ad67dfc831c99e34a51d036
# Parent  3fa321cbc337f8dd0bccd3273935f9535062177d
...

diff -r 3fa321cbc337 -r 6bf0899a6150 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 23 10:33:47 2022 +0900
+++ b/src/zorn.agda	Tue Aug 23 11:25:55 2022 +0900
@@ -783,6 +783,17 @@
              field
                 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 
 
+          initial-segment : {a b z : Ordinal } → (a<x : a o< x )   → (b<x : b o< x )   
+              →  a o≤ b 
+              →  ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z o≤  ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
+          initial-segment = ?
+
+          is01 : {a b : Ordinal } → (a<x : a o< x )   → (b<x : b o< x )   
+              →  a o≤ b 
+              UnionCF A f mf ay (ZChain.supf (pzc (osuc a) (ob<x lim a<x ))) x ⊆'
+              UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim b<x ))) x 
+          is01 = ?
+
           supf1 : Ordinal → Ordinal
           supf1 z = ?
           -- ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z