Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 852:a28bb57c88e6

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 06 Sep 2022 01:18:54 +0900
parents	717b8c3f55c9
children	2569ace27176

comparison

equal deleted inserted replaced

-:717b8c3f55c9
+:a28bb57c88e6
 supf0=1 {px} {z} z≤px with trio< z px
 ... | tri< a ¬b ¬c = refl
 ... | tri≈ ¬a b ¬c = refl
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
+supfx : {z : Ordinal } → z ≡ x →  supf0 px ≡ supf1 px z
+supfx {z} z=x with trio< z px
+... | tri< a ¬b ¬c = ⊥-elim ( o<¬≡ z=x (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
+... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ z=x (subst (λ k → k o< x ) (sym b) (pxo<x op)))
+... | tri> ¬a ¬b c = refl
 supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 px b)
 supf∈A {b} b≤z with trio< b px
 ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a ))
 ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b ))
 ... | tri> ¬a ¬b c = proj1 ( ZChain.csupf zc o≤-refl )
 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
 zcsup with zc30
 ... | 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 px) (supf1 px b)) (supf1 px b)
-csupf {b} b≤x = ⟪ zc01 , ch-is-sup u o≤-refl
+csupf {b} b≤x = zc05 where
-record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc  ⟫  where
-csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 px b)) (supf1 px b)
-csupf0 b≤px = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
 zc04 : (b o≤ px ) ∨ (b ≡ x )
 zc04 with trio< b px
 ... | tri< a ¬b ¬c = case1 (o<→≤ a)
 ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
 ... | case1 eq = case2 eq
 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
-zc01 : odef A (supf1 px b)
+zc05 : odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b)
-zc01 = supf∈A b≤x
+zc05 with zc04
-u = supf1 px b
+... | case2 b=x with ZChain.csupf zc o≤-refl
-supu=u : supf1 px u ≡ u
+... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au
-supu=u with zc04
+, ch-init (subst₂ (λ j k → FClosure A f j k  ) refl (supfx b=x) fc) ⟫
-... | case2 eq = begin
+... | ⟪ au , ch-is-sup u u≤x is-sup fc  ⟫  = ⟪ subst (λ k → odef A k) (supfx b=x) au
-supf1 px u ≡⟨ ? ⟩
+, ch-is-sup u (subst (λ k → u o≤ k) (supfx b=x) u≤x) ? zc06 ⟫ where
-supf0 px ≡⟨ ? ⟩
+zc06 : FClosure A f (supf1 px u)  (supf1 px b)
-u ∎ where open ≡-Reasoning
+zc06 = ?
-... | case1 le = ? where
+zc07 : FClosure A f (supf0 u)  (supf0 px)
-zc06 : b o≤ px
+zc07 = fc
-zc06 = le
+zc05 | case1 b≤px with ZChain.csupf zc b≤px
-zc02 : odef A (supf1 px u)
+... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au
-zc02 = subst (λ k → odef A k ) (sym supu=u) zc01
+, ch-init (subst₂ (λ j k → FClosure A f j k  ) refl (supf0=1 b≤px) fc) ⟫
-zc03 : supf1 px u ≡ supf1 px b
+... | ⟪ au , ch-is-sup u u≤x is-sup fc  ⟫  = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au
-zc03 = ?
+, ch-is-sup u (subst (λ k → u o≤ k) (supf0=1 b≤px) u≤x) ? zc06 ⟫ where
-fc : FClosure A f (supf1 px u) (supf1 px b)
+zc06 : FClosure A f (supf1 px u)  (supf1 px b)
-fc = init zc02 zc03
+zc06 = ?
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u)
+zc07 : FClosure A f (supf0 u)  (supf0 b)
-fcy<sup = ?
+zc07 = fc
-order : {s z1 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z1
-→ (z1 ≡ supf1 px u) ∨ (z1 << supf1 px u)
-order = ?
 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px z ≡ & (SUP.sup (sup z≤x))
 sis {z} z≤x  = zc40 where
 zc40 : supf1 px z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error
 zc40 with trio< z px | inspect (supf1 px) z | inspect sup z≤x
 ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?

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

comparison src/zorn.agda @ 852:a28bb57c88e6