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

comparison src/zorn.agda @ 847:bf1b6c4768d2

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 Sat, 03 Sep 2022 13:28:10 +0900
parents 95bbeb622f6e
children 56a150965988
comparison
equal deleted inserted replaced
846:95bbeb622f6e 847:bf1b6c4768d2
971 csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px ) 971 csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
972 csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) 972 csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
973 csupf1 with csupf0 973 csupf1 with csupf0
974 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 974 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
975 ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ 975 ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫
976 = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = ? } ? ⟫ where 976 = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = supu=u1 } ? ⟫ where
977 zc13 : supf0 u o< supf0 b
978 zc13 = ?
979 zc12 : odef (UnionCF A f mf ay supf0 b) (supf1 b)
980 zc12 = subst (λ k → odef (UnionCF A f mf ay supf0 b) k) &iso ( ZChain.csupf-fc zc b≤px zc13 fc )
977 u≤x1 : u o≤ supf1 b 981 u≤x1 : u o≤ supf1 b
978 u≤x1 = u≤x 982 u≤x1 = u≤x
983 supu=u0 : supf0 u ≡ u
984 supu=u0 = supu=u
979 supu=u1 : supf1 u ≡ u 985 supu=u1 : supf1 u ≡ u
980 supu=u1 = ? 986 supu=u1 with trio< u px
987 ... | tri< a ¬b ¬c = supu=u
988 ... | tri≈ ¬a b ¬c = supu=u
989 ... | tri> ¬a ¬b c = ? -- supf1 b ≡ sp1 , u o≤ sp1, x o≤ u o≤ supf1 b -- u ≡ x → xsup x → ⊥
990 -- u > x → supf1 u ≡ sp1 → supf1 b o≤ supf1 u
991 -- px o< u o≤ sp1 , spuf1 u o≤ spuf1 sp1
981 fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) 992 fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
982 fcy<sup1 = ? 993 fcy<sup1 = ?
983 order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 994 order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1
984 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) 995 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
985 order1 = ? 996 order1 = ?