Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 846:95bbeb622f6e
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 03 Sep 2022 09:43:19 +0900 (2022-09-03) |
parents | ef7c721b32dc |
children | bf1b6c4768d2 |
files | src/zorn.agda |
diffstat | 1 files changed, 34 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Aug 31 22:08:33 2022 +0900 +++ b/src/zorn.agda Sat Sep 03 09:43:19 2022 +0900 @@ -311,13 +311,6 @@ supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b) supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) ) - csupf0 : {b : Ordinal} → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) - csupf0 {b} b≤z = ⟪ supf∈A b≤z , ch-is-sup (supf b) o≤-refl ? (init zc10 zc11 ) ⟫ where - zc11 : supf (supf b) ≡ supf b - zc11 = ? - zc10 : odef A (supf (supf b)) - zc10 = subst (λ k → odef A k ) (sym zc11) ( supf∈A b≤z ) - fcy<sup : {u w : Ordinal } → u o< z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf fcy<sup {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ @@ -781,6 +774,9 @@ ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c ) + supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b) + supf∈A {b} b≤z = ? + supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1 supf1≤sp1 = ? @@ -967,7 +963,37 @@ ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } } csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) - csupf {b} b≤x = ? + csupf {b} b≤x with osuc-≡< b≤x + ... | case2 b<x = csupf1 where + b≤px : b o≤ px + b≤px = zc-b<x _ b<x + csupf0 : odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b) + csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px ) + csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) + csupf1 with csupf0 + ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ + ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ + = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = ? } ? ⟫ where + u≤x1 : u o≤ supf1 b + u≤x1 = u≤x + supu=u1 : supf1 u ≡ u + supu=u1 = ? + fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) + fcy<sup1 = ? + order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 + → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) + order1 = ? + ... | case1 refl = ⟪ supf∈A o≤-refl , ch-is-sup (supf1 x) o≤-refl + record { fcy<sup = fcy<sup ; order = order ; supu=u = zc11 } (init zc10 zc11 ) ⟫ where + zc11 : supf1 (supf1 x) ≡ supf1 x + zc11 = ? + zc10 : odef A (supf1 (supf1 x)) + zc10 = subst (λ k → odef A k ) (sym zc11) ( supf∈A o≤-refl ) + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 (supf1 x)) ∨ (z << supf1 (supf1 x)) + fcy<sup = ? + order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → FClosure A f (supf1 s) z1 + → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b)) + order = ? sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) sis {z} z≤x = zc40 where zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error