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

comparison src/zorn.agda @ 851:717b8c3f55c9

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 05 Sep 2022 21:54:55 +0900
parents	2d8ce664ae31
children	a28bb57c88e6

comparison

equal deleted inserted replaced

-:2d8ce664ae31
+:717b8c3f55c9
 pcy : odef pchain y
 pcy = ⟪ ay , ch-init (init ay refl)    ⟫
 supf0 = ZChain.supf zc
-supf1 : Ordinal → Ordinal
+supf1 : (px z : Ordinal) → Ordinal
-supf1 z with trio< z px
+supf1 px z with trio< z px
 ... | tri< a ¬b ¬c = ZChain.supf zc z
 ... | tri≈ ¬a b ¬c = ZChain.supf zc z
 ... | tri> ¬a ¬b c = ZChain.supf zc px
 pchain1 : HOD
-pchain1  = UnionCF A f mf ay supf1 x
+pchain1  = UnionCF A f mf ay (supf1 px) x
 ptotal1 : IsTotalOrderSet pchain1
 ptotal1 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
+uz01 = chain-total A f mf ay (supf1 px) ( (proj2 ca)) ( (proj2 cb))
 pchain⊆A1 : {y : Ordinal} → odef pchain1 y →  odef A y
 pchain⊆A1 {y} ny = proj1 ny
 pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
 pnext1 {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
 pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
 pinit1 :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
 pinit1 {a} ⟪ aa , ua ⟫  with  ua
 ... | ch-init fc = s≤fc y f mf fc
 ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-zc7 : y <= supf1 u
+zc7 : y <= supf1 px u
 zc7 = ChainP.fcy<sup is-sup (init ay refl)
 pcy1 : odef pchain1 y
 pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
-supf0=1 : {z : Ordinal } → z o≤ px  → supf0 z ≡ supf1 z
+supf0=1 : {px z : Ordinal } → z o≤ px  → supf0 z ≡ supf1 px z
-supf0=1 {z} z≤px with trio< z px
+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 )
-supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b)
+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 )
-supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
+supf-mono : {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b
 supf-mono = ?
-zc70 : HasPrev A pchain x f → ¬ xSUP pchain x
+fc0→1 : {px s z : Ordinal } → s o≤ px  → FClosure A f (supf0 s) z → FClosure A f (supf1 px s) z
-zc70 pr xsup = ?
+fc0→1 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc
-fc0→1 : {s z : Ordinal } → s o≤ px  → FClosure A f (supf0 s) z → FClosure A f (supf1 s) z
+fc1→0 : {px s z : Ordinal } → s o≤ px  → FClosure A f (supf1 px s) z → FClosure A f (supf0 s) z
-fc0→1 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc
+fc1→0 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc
-fc1→0 : {s z : Ordinal } → s o≤ px  → FClosure A f (supf1 s) z → FClosure A f (supf0 s) z
+CP0→1 : {px u : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b)
-fc1→0 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc
+→ u o≤ px  → ChainP A f mf ay supf0 u → ChainP A f mf ay (supf1 px) u
+CP0→1 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where
-CP0→1 : {u : Ordinal } → u o≤ px  → ChainP A f mf ay supf0 u → ChainP A f mf ay supf1 u
+fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u )
-CP0→1 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u )
 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (supf0=1 u≤px) ( ChainP.fcy<sup cp fc )
-order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z2 →
+order : {s : Ordinal} {z2 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z2 →
-(z2 ≡ supf1 u) ∨ (z2 << supf1 u)
+(z2 ≡ supf1 px u) ∨ (z2 << supf1 px u)
 order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (supf0=1 u≤px) ( ChainP.order cp ss<su (fc1→0 s≤px fc )) where
 s≤px : s o≤ px
 s≤px = ordtrans (supf-inject0 supf-mono s<u) u≤px
 ss<su : supf0 s o< supf0 u
 ss<su = subst₂ (λ j k → j o< k ) (sym (supf0=1 s≤px )) (sym (supf0=1 u≤px)) s<u
-CP1→0 : {u : Ordinal } → u o≤ px  → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u
+CP1→0 : {px u : Ordinal } → ( {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b)
-CP1→0 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where
+→ u o≤ px  → ChainP A f mf ay (supf1 px) u → ChainP A f mf ay supf0 u
+CP1→0 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where
 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u )
 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym (supf0=1 u≤px)) ( ChainP.fcy<sup cp fc )
 order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z2 →
 (z2 ≡ supf0 u) ∨ (z2 << supf0 u)
 order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym (supf0=1 u≤px)) ( ChainP.order cp ss<su (fc0→1 s≤px fc )) where
 s≤px : s o≤ px
 s≤px = ordtrans (supf-inject0 (ZChain.supf-mono zc) s<u) u≤px
-ss<su : supf1 s o< supf1 u
+ss<su : supf1 px s o< supf1 px u
 ss<su = subst₂ (λ j k → j o< k ) (supf0=1 s≤px ) (supf0=1 u≤px) s<u
-UnionCF0⊆1  : {z : Ordinal } → z o≤ px →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 z
+UnionCF0⊆1  : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay (supf1 px) z
-UnionCF0⊆1  {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
+UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
-UnionCF0⊆1  {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ =
+UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ =
-⟪ au , ch-is-sup u u≤z (CP0→1 (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫
+⟪ au , ch-is-sup u u≤z (CP0→1 supf-mono (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫
-UnionCF1⊆0  : {z : Ordinal } → z o≤ px →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 z
+UnionCF1⊆0  : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px →  UnionCF A f mf ay (supf1 px) z ⊆' UnionCF A f mf ay supf0 z
-UnionCF1⊆0  {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
+UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
-UnionCF1⊆0  {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ =
+UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ =
-⟪ au , ch-is-sup u u≤z (CP1→0 (OrdTrans u≤z z≤px ) is-sup)
+⟪ au , ch-is-sup u u≤z (CP1→0 supf-mono (OrdTrans u≤z z≤px ) is-sup)
 (fc1→0 (OrdTrans u≤z z≤px ) fc) ⟫
 -- zc100  : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1
 -- zc100  = ?
 -- if previous chain satisfies maximality, we caan reuse it
 --
 --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
 no-extension : ¬ xSUP (UnionCF A f mf ay supf0 px) x → ZChain A f mf ay x
-no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = supf-mono
+no-extension ¬sp=x = record { supf = supf1 px ;  sup = sup ; supf-mono = supf-mono
 ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
 ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
 pchain0=1 : pchain ≡ pchain1
 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 u1≤x u1-is-sup)  (fc0→1 u1≤x fc)  ⟫
+zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 supf-mono u1≤x u1-is-sup)  (fc0→1 u1≤x fc)  ⟫
 zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
 zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x
-... | case1 eq = ⊥-elim (¬sp=x zcsup) where
+... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 supf-mono u1≤px u1-is-sup)  (fc1→0 u1≤px fc)  ⟫ where
-x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
-x<sup = ?
-zc12 : supf1 x ≡ u1
-zc12 = subst  (λ k → supf1 k ≡ u1) eq  (ChainP.supu=u u1-is-sup)
-zcsup : xSUP (UnionCF A f mf ay supf0 px) x
-zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) ; is-sup = record { x<sup = x<sup } }
-... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 u1≤px u1-is-sup)  (fc1→0 u1≤px fc)  ⟫ where
 u1≤px : u1 o≤ px
 u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt)
-sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
+... | case1 eq = ⊥-elim (¬sp=x zcsup) where
-sup {z} z≤x with trio< z px | inspect supf1 z
+s1u=x : supf1 px u1 ≡ x
-... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o<→≤ a)) (ZChain.sup zc (o<→≤ a) )
+s1u=x = trans (ChainP.supu=u u1-is-sup) eq
-... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) )
+zc13 : osuc px o< osuc u1
-... | tri> ¬a ¬b px<z | record { eq = eq1} = ? where
+zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq) )
+x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
+x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x
+( ChainP.fcy<sup u1-is-sup {w} fc  )
+x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans u≤x zc13 ))
+... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 u≤x ) where
+zc14 : u ≡ osuc px
+zc14 = begin
+u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩
+supf0 u ≡⟨ supf0=1 u≤x ⟩
+supf1 px u ≡⟨ eq1 ⟩
+supf1 px u1 ≡⟨ s1u=x ⟩
+x ≡⟨ sym (Oprev.oprev=x op) ⟩
+osuc px ∎ where open ≡-Reasoning
+... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt (fc0→1 u≤x fc) )
+zc12 : supf1 px x ≡ u1
+zc12 = subst  (λ k → supf1 px k ≡ u1) eq  (ChainP.supu=u u1-is-sup)
+zcsup : xSUP (UnionCF A f mf ay supf0 px) x
+zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl)
+; is-sup = record { x<sup = x<sup } }
+sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay (supf1 px) z)
+sup {z} z≤x with trio< z px | inspect (supf1 px) z
+... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o<→≤ a)) (ZChain.sup zc (o<→≤ a) )
+... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) )
+... | tri> ¬a ¬b px<z | record { eq = eq1} = subst (λ k → SUP A k )
+(trans pchain0=1 (cong (λ k → UnionCF A f mf ay (supf1 px) k ) (sym zc30) )) (ZChain.sup zc o≤-refl ) where
 zc30 : z ≡ x
 zc30 with osuc-≡< z≤x
 ... | case1 eq = eq
 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
 sup=u : {b : Ordinal} (ab : odef A b) →
-b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
+b o≤ x → IsSup A (UnionCF A f mf ay (supf1 px) b) ab → (supf1 px) b ≡ b
 sup=u {b} ab b≤x is-sup with trio< b px
-... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o<→≤ a) lt) }
+... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o<→≤ a) lt) }
-... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o≤-refl0 b) lt) }
+... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o≤-refl0 b) lt) }
 ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
 zc30 : x ≡ b
 zc30 with osuc-≡< b≤x
 ... | case1 eq = sym (eq)
 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
 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 (supf1 b)) (supf1 b)
+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
 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 b)) (supf1 b)
+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 b)
+zc01 : odef A (supf1 px b)
-zc01 with zc04
+zc01 = supf∈A b≤x
-... | case1 le = proj1 ( csupf0 le )
+u = supf1 px b
-... | case2 eq = ? -- subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1)
+supu=u : supf1 px u ≡ u
-u = supf1 b
-supu=u : supf1 u ≡ u
 supu=u with zc04
 ... | case2 eq = begin
-supf1 u ≡⟨ ? ⟩
+supf1 px u ≡⟨ ? ⟩
+supf0 px ≡⟨ ? ⟩
 u ∎ where open ≡-Reasoning
-... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? )  where
+... | case1 le = ? where
 zc06 : b o≤ px
 zc06 = le
-zc05 : supf1 b o≤ px
+zc02 : odef A (supf1 px u)
-zc05 = ?
-zc02 : odef A (supf1 u)
 zc02 = subst (λ k → odef A k ) (sym supu=u) zc01
-zc03 : supf1 u ≡ supf1 b
+zc03 : supf1 px u ≡ supf1 px b
 zc03 = ?
-fc : FClosure A f (supf1 u) (supf1 b)
+fc : FClosure A f (supf1 px u) (supf1 px b)
 fc = init zc02 zc03
-fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
+fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u)
 fcy<sup = ?
-order : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1
+order : {s z1 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z1
-→ (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
+→ (z1 ≡ supf1 px u) ∨ (z1 << supf1 px u)
 order = ?
-sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
+sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px 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
+zc40 : supf1 px z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error
-zc40 with trio< z px | inspect supf1 z | inspect sup z≤x
+zc40 with trio< z px | inspect (supf1 px) z | inspect sup z≤x
 ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
 ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ?
 zc4 : ZChain A f mf ay x
 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f )
 -- we have to check adding x preserve is-max ZChain A y f mf x
 ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
 ... | case1 is-sup = -- x is a sup of zc
-record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
+record {  supf = supf1 x ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
 ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
 supx : SUP A (UnionCF A f mf ay supf0 x)
 supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
 spx = & (SUP.sup supx )
 x=spx : x ≡ spx
 x=spx = sym &iso
 psupf1 : Ordinal → Ordinal
-psupf1 z with trio< z x
+psupf1 z = supf1 x z
-... | tri< a ¬b ¬c = ZChain.supf zc z
-... | tri≈ ¬a b ¬c = x
-... | tri> ¬a ¬b c = x
 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
 csupf {b} b≤x with trio< b px | inspect psupf1 b
 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
 ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} where -- b ≡ x, supf x ≡ sp

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

comparison src/zorn.agda @ 851:717b8c3f55c9