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

comparison src/zorn.agda @ 1035:2144ef00cab9

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, 02 Dec 2022 11:07:51 +0900
parents 84881efe649b
children 23a8e4d558e0
comparison
equal deleted inserted replaced
1034:84881efe649b 1035:2144ef00cab9
264 ... | case1 eq = trans eq (sym a=b) 264 ... | case1 eq = trans eq (sym a=b)
265 ... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-≤ lt fc00 ) ) where 265 ... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-≤ lt fc00 ) ) where
266 fc00 : b ≤ (f b) 266 fc00 : b ≤ (f b)
267 fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa )) 267 fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
268 268
269 fc-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) (supf : Ordinal → Ordinal )
270 (order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y)
271 {s s1 a b : Ordinal } ( fa : FClosure A f (supf s) a )( fb : FClosure A f (supf s1) b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
272 fc-total A f mf supf order {xa} {xb} {a} {b} ca cb with trio< xa xb
273 ... | tri< a₁ ¬b ¬c with ≤-ftrans (order a₁ ca ) (s≤fc (supf xb) f mf cb )
274 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
275 ct00 : * a ≡ * b
276 ct00 = cong (*) eq1
277 ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
278 fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri≈ _ refl _ = fcn-cmp _ f mf ca cb
279 fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri> ¬a ¬b c with ≤-ftrans (order c cb ) (s≤fc (supf xa) f mf ca )
280 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
281 ct00 : * a ≡ * b
282 ct00 = cong (*) (sym eq1)
283 ... | case2 b<a = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a
284
285 269
286 ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A 270 ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
287 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 271 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
288 272
289 -- Union of supf z and FClosure A f y 273 -- Union of supf z and FClosure A f y
347 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 331 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
348 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 332 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
349 field 333 field
350 supf : Ordinal → Ordinal 334 supf : Ordinal → Ordinal
351 335
352 order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y 336 order : {x y w : Ordinal } → y o≤ z → x o< y → FClosure A f (supf x) w → w ≤ supf y
353 337
354 cfcs : (mf< : <-monotonic-f A f) 338 cfcs : (mf< : <-monotonic-f A f)
355 {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w 339 {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
356 340
357 asupf : {x : Ordinal } → odef A (supf x) 341 asupf : {x : Ordinal } → odef A (supf x)
406 initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc 390 initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc
407 initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc) 391 initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc)
408 392
409 f-total : IsTotalOrderSet chain 393 f-total : IsTotalOrderSet chain
410 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = 394 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
411 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fc-total A f mf supf order fca fcb) 395 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
396 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
397 fc-total with trio< ua ub
398 ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) a₁ fca ) (s≤fc (supf ub) f mf fcb )
399 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
400 ct00 : * (& a) ≡ * (& b)
401 ct00 = cong (*) eq1
402 ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
403 fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
404 fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) c fcb ) (s≤fc (supf ua) f mf fca )
405 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
406 ct00 : * (& a) ≡ * (& b)
407 ct00 = cong (*) (sym eq1)
408 ... | case2 b<a = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a
412 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where 409 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
413 ft01 : (& a) ≤ (& b) → Tri ( a < b) ( a ≡ b) ( b < a ) 410 ft01 : (& a) ≤ (& b) → Tri ( a < b) ( a ≡ b) ( b < a )
414 ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where 411 ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where
415 a=b : a ≡ b 412 a=b : a ≡ b
416 a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) 413 a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq)
453 450
454 supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b 451 supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b
455 supf-idem mf< {b} b≤z sfb≤x = z52 where 452 supf-idem mf< {b} b≤z sfb≤x = z52 where
456 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) 453 z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
457 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc 454 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
458 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order su<b fc where 455 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b fc where
459 su<b : u o< b 456 su<b : u o< b
460 su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) 457 su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
461 z52 : supf (supf b) ≡ supf b 458 z52 : supf (supf b) ≡ supf b
462 z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 459 z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
463 460
853 sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) 850 sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
854 851
855 m13 : supf0 px o≤ sp1 852 m13 : supf0 px o≤ sp1
856 m13 = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where 853 m13 = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where
857 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) 854 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
858 m14 {z} ⟪ as , ch-init fc ⟫ = ? 855 m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) sfpx≤sp1
859 m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ? 856 m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) sfpx≤sp1
860 857
861 zc41 : ZChain A f mf ay x 858 zc41 : ZChain A f mf ay x
862 zc41 with zc43 x sp1 859 zc41 with zc43 x sp1
863 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ? 860 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ?
864 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where 861 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where
1031 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 1028 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
1032 ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫ 1029 ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫
1033 ... | case2 fc = case2 (fsuc _ fc) 1030 ... | case2 fc = case2 (fsuc _ fc)
1034 zc21 (init asp refl ) = ? 1031 zc21 (init asp refl ) = ?
1035 1032
1036 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where 1033 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
1037 field 1034 is-minsup {z} z≤x with osuc-≡< z≤x
1038 tsup : MinSUP A (UnionCF A f ay supf1 z) 1035 ... | case1 z<x = ZChain.is-minsup zc (zc-b<x z<x)
1039 tsup=sup : supf1 z ≡ MinSUP.sup tsup 1036 ... | case2 z=x = ?
1040 1037
1041 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x 1038 order : {a b : Ordinal} {w : Ordinal} →
1042 sup {z} z≤x with trio< z px 1039 b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b
1043 ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.as m 1040 order {a} {b} {w} b≤x a<b fc with trio< b px
1044 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where 1041 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) ))
1045 m = ZChain.minsup zc (o<→≤ a) 1042 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
1046 ms00 : {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) 1043 ... | tri> ¬a ¬b px<b with trio< a px
1047 ms00 {w} ⟪ az , cp ⟫ = MinSUP.x≤sup m ⟪ az , ? ⟫ 1044 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) sfpx≤sp1 -- supf1 a ≡ supf0 a
1048 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 1045 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc ))
1049 odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 1046 ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where -- supf1 a ≡ sp1
1050 ms01 {sup2} us P = MinSUP.minsup m us ? 1047 zc22 : a o< osuc px
1051 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.as m 1048 zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
1052 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where
1053 m = ZChain.minsup zc (o≤-refl0 b)
1054 ms00 : {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
1055 ms00 {x} ux = MinSUP.x≤sup m ?
1056 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
1057 odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
1058 ms01 {sup2} us P = MinSUP.minsup m us ?
1059 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.as sup1
1060 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
1061 m = sup1
1062 ms00 : {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
1063 ms00 {x} ux = MinSUP.x≤sup m ?
1064 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
1065 odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
1066 ms01 {sup2} us P = MinSUP.minsup m us ?
1067
1068 1049
1069 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc ; order = ? 1050 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc ; order = ?
1070 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where 1051 ; supfmax = ? ; sup=u = ? ; is-minsup = ? ; cfcs = cfcs } where
1071 1052
1072 -- supf0 px not is included by the chain 1053 -- supf0 px not is included by the chain
1073 -- supf1 x ≡ supf0 px because of supfmax 1054 -- supf1 x ≡ supf0 px because of supfmax
1074 1055
1075 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 1056 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
1170 ... | tri< a ¬b ¬c = zc36 ¬b 1151 ... | tri< a ¬b ¬c = zc36 ¬b
1171 ... | tri> ¬a ¬b c = zc36 ¬b 1152 ... | tri> ¬a ¬b c = zc36 ¬b
1172 ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ? } where 1153 ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ? } where
1173 zc37 : MinSUP A (UnionCF A f ay supf0 z) 1154 zc37 : MinSUP A (UnionCF A f ay supf0 z)
1174 zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? } 1155 zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? }
1156
1157 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
1158 is-minsup = ?
1159
1175 sup=u : {b : Ordinal} (ab : odef A b) → 1160 sup=u : {b : Ordinal} (ab : odef A b) →
1176 b o≤ x → IsMinSUP A (UnionCF A f ay supf0 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf0 b) f b ) → supf0 b ≡ b 1161 b o≤ x → IsMinSUP A (UnionCF A f ay supf0 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf0 b) f b ) → supf0 b ≡ b
1177 sup=u {b} ab b≤x is-sup with trio< b px 1162 sup=u {b} ab b≤x is-sup with trio< b px
1178 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫ 1163 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫
1179 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫ 1164 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫
1187 zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) 1172 zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
1188 zc32 = ? 1173 zc32 = ?
1189 1174
1190 ... | no lim with trio< x o∅ 1175 ... | no lim with trio< x o∅
1191 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 1176 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
1192 ... | tri≈ ¬a b ¬c = record { supf = ? } 1177 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
1178 ; supfmax = ? ; is-minsup = ? ; cfcs = ? }
1193 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ? 1179 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
1194 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where 1180 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where
1195 1181
1196 pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z 1182 pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
1197 pzc {z} z<x = prev z z<x 1183 pzc {z} z<x = prev z z<x
1198 1184
1199 ysp = MinSUP.sup (ysup f mf ay) 1185 ysp = MinSUP.sup (ysup f mf ay)
1225 ptotalx : IsTotalOrderSet pchainx 1211 ptotalx : IsTotalOrderSet pchainx
1226 ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1212 ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1227 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1213 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1228 uz01 with trio< (IChain.i ia) (IChain.i ib) 1214 uz01 with trio< (IChain.i ia) (IChain.i ib)
1229 ... | tri< ia<ib ¬b ¬c with 1215 ... | tri< ia<ib ¬b ¬c with
1230 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib)) 1216 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
1231 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 1217 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
1232 ct00 : * (& a) ≡ * (& b) 1218 ct00 : * (& a) ≡ * (& b)
1233 ct00 = cong (*) eq1 1219 ct00 = cong (*) eq1
1234 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1) 1220 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
1235 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) 1221 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
1236 uz01 | tri> ¬a ¬b ib<ia with 1222 uz01 | tri> ¬a ¬b ib<ia with
1237 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia)) 1223 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
1238 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 1224 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
1239 ct00 : * (& a) ≡ * (& b) 1225 ct00 : * (& a) ≡ * (& b)
1240 ct00 = sym (cong (*) eq1) 1226 ct00 = sym (cong (*) eq1)
1241 ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt 1227 ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt
1242 1228
1284 supf-mono : {x y : Ordinal } → x o≤ y → supf1 x o≤ supf1 y 1270 supf-mono : {x y : Ordinal } → x o≤ y → supf1 x o≤ supf1 y
1285 supf-mono {x} {y} x≤y with trio< y x 1271 supf-mono {x} {y} x≤y with trio< y x
1286 ... | tri< a ¬b ¬c = ? 1272 ... | tri< a ¬b ¬c = ?
1287 ... | tri≈ ¬a b ¬c = ? 1273 ... | tri≈ ¬a b ¬c = ?
1288 ... | tri> ¬a ¬b c = ? 1274 ... | tri> ¬a ¬b c = ?
1275
1276 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
1277 is-minsup = ?
1289 1278
1290 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 1279 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
1291 → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w 1280 → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
1292 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x 1281 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
1293 ... | case1 b=x with trio< a x 1282 ... | case1 b=x with trio< a x
1377 z13 : * (& s) < * sp 1366 z13 : * (& s) < * sp
1378 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ? ) 1367 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ? )
1379 ... | case1 eq = ⊥-elim ( ne eq ) 1368 ... | case1 eq = ⊥-elim ( ne eq )
1380 ... | case2 lt = lt 1369 ... | case2 lt = lt
1381 z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp 1370 z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp
1382 z19 = record { x≤sup = z20 } where 1371 z19 = record { ax = ? ; x≤sup = z20 } where
1383 z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) 1372 z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
1384 z20 {y} zy with MinSUP.x≤sup sp1 1373 z20 {y} zy with MinSUP.x≤sup sp1
1385 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22) zy )) 1374 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22) zy ))
1386 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) 1375 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )
1387 ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p ) 1376 ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p )