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

comparison src/zorn.agda @ 862:269467244745

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 Fri, 09 Sep 2022 08:19:50 +0900
parents 4e60b42b83a3
children f5fc3f5f618f
comparison
equal deleted inserted replaced
861:4e60b42b83a3 862:269467244745
880 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f ) 880 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f )
881 -- we have to check adding x preserve is-max ZChain A y f mf x 881 -- we have to check adding x preserve is-max ZChain A y f mf x
882 ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next 882 ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
883 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) 883 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
884 ... | case1 is-sup = -- x is a sup of zc 884 ... | case1 is-sup = -- x is a sup of zc
885 record { supf = supf1 885 record { supf = supf1 ; supf-max = ?
886 ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!} 886 ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
887 ; sup = {!!} ; supf-is-sup = {!!} } where 887 ; sup = {!!} ; supf-is-sup = {!!} } where
888 supf1 : Ordinal → Ordinal 888 supf1 : Ordinal → Ordinal
889 supf1 z with trio< z px 889 supf1 z with trio< z px
890 ... | tri< a ¬b ¬c = ZChain.supf zc z 890 ... | tri< a ¬b ¬c = ZChain.supf zc z
891 ... | tri≈ ¬a b ¬c = ZChain.supf zc z 891 ... | tri≈ ¬a b ¬c = ZChain.supf zc z
892 ... | tri> ¬a ¬b c = x 892 ... | tri> ¬a ¬b c = x --- SUP A (UnionCF A f mf ay supf0 px) ≡ SUP A (UnionCF A f mf ay supf1 px)
893 893
894 pchainx : HOD 894 pchainx : HOD
895 pchainx = UnionCF A f mf ay supf1 x 895 pchainx = UnionCF A f mf ay supf1 x
896 896
897 supf0px=x : supf0 px ≡ x 897 supf0px=x : (ax : odef A x) → IsSup A (ZChain.chain zc ) ax → x ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
898 supf0px=x = ? where 898 supf0px=x is-sup = ? where
899 zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) ) 899 zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
900 zc50 = ZChain.spuf-is-sup zc ? 900 zc50 = ZChain.supf-is-sup zc ?
901 901
902 supf-monox : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 902 supf-monox : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
903 supf-monox {i} {j} i≤j with trio< i px | trio< j px 903 supf-monox {i} {j} i≤j with trio< i px | trio< j px
904 ... | tri< a ¬b ¬c | tri< ja ¬jb ¬jc = ? 904 ... | tri< a ¬b ¬c | tri< ja ¬jb ¬jc = ?
905 ... | tri< a ¬b ¬c | tri≈ ¬ja jb ¬jc = ? 905 ... | tri< a ¬b ¬c | tri≈ ¬ja jb ¬jc = ?
919 supfx1 {z} x≤z with trio< z px 919 supfx1 {z} x≤z with trio< z px
920 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc ))) 920 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
921 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op))) 921 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
922 ... | tri> ¬a ¬b c = refl 922 ... | tri> ¬a ¬b c = refl
923 923
924 pchain0=x : UnionCF A f mf ay supf0 px ≡ UnionCF A f mf ay supf1 px
925 pchain0=x = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
926 zc10 : {z : Ordinal} → OD.def (od pchain) z → odef (UnionCF A f mf ay supf1 px) z
927 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
928 zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ? ⟫
929 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 px) z → OD.def (od pchain) z
930 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
931 zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ?
932
924 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) 933 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
925 csupf {b} b≤x with zc04 b≤x 934 csupf {b} b≤x with zc04 b≤x
926 ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫ 935 ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫
927 ... | case1 b≤px with ZChain.csupf zc b≤px 936 ... | case1 b≤px with ZChain.csupf zc b≤px
928 ... | ⟪ au , ch-init fc ⟫ = ⟪ ? , ch-init ? ⟫ 937 ... | ⟪ au , ch-init fc ⟫ = ⟪ ? , ch-init ? ⟫