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

comparison src/zorn.agda @ 953:dfb4f7e9c454

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 Wed, 02 Nov 2022 03:42:53 +0900
parents 05f54e16f138
children e43a5cc72287
comparison
equal deleted inserted replaced
952:05f54e16f138 953:dfb4f7e9c454
78 <-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z 78 <-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
79 <-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y 79 <-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
80 <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) 80 <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
81 81
82 ftrans<=-< : {x y z : Ordinal } → x <= y → y << z → x << z 82 ftrans<=-< : {x y z : Ordinal } → x <= y → y << z → x << z
83 ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) ? y<z 83 ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq)) y<z
84 ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z 84 ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z
85 85
86 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y 86 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y
87 <=to≤ (case1 eq) = case1 (cong (*) eq) 87 <=to≤ (case1 eq) = case1 (cong (*) eq)
88 <=to≤ (case2 lt) = case2 lt 88 <=to≤ (case2 lt) = case2 lt
580 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫ 580 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
581 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) 581 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx )
582 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ 582 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫
583 583
584 -- 584 --
585 -- Second TransFinite Pass for maximality 585 -- maximality of chain
586 --
587 -- supf is fixed for z ≡ & A , we can prove order and is-max
586 -- 588 --
587 589
588 SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 590 SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
589 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x 591 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x
590 SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where 592 SZ1 f mf {y} ay zc x = zc1 x where
591 chain-mono1 : {a b c : Ordinal} → a o≤ b 593 chain-mono1 : {a b c : Ordinal} → a o≤ b
592 → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c 594 → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
593 chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b 595 chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
594 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) 596 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b)
595 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f 597 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f
632 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) 634 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
633 zc04 with zc00 635 zc04 with zc00
634 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq ) 636 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq )
635 ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt ) 637 ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
636 638
637 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x 639 zc1 : (x : Ordinal) → ZChain1 A f mf ay zc x
638 zc1 x prev with Oprev-p x -- prev is not used now.... 640 zc1 x with Oprev-p x -- prev is not used now....
639 ... | yes op = record { is-max = is-max ; order = order } where 641 ... | yes op = record { is-max = is-max ; order = order } where
640 px = Oprev.oprev op 642 px = Oprev.oprev op
641 zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px 643 zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
642 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt ) 644 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt )
643 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → 645 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
864 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc 866 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
865 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z 867 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
866 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 868 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
867 zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where 869 zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
868 u<x : u o< x 870 u<x : u o< x
869 u<x = ? 871 u<x = supf-inject0 supf1-mono su<sx
872 u≤px : u o≤ px
873 u≤px = zc-b<x _ u<x
870 zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 874 zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
871 zc21 {z1} (fsuc z2 fc ) with zc21 fc 875 zc21 {z1} (fsuc z2 fc ) with zc21 fc
872 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 876 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
873 ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 877 ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
874 ... | case2 fc = case2 (fsuc _ fc) 878 ... | case2 fc = case2 (fsuc _ fc)
875 zc21 (init asp refl ) with trio< u px | inspect supf1 u 879 zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u
876 ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 880 ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
877 ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where 881 ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
882 u<px : u o< px
883 u<px = ZChain.supf-inject zc a
884 asp0 : odef A (supf0 u)
885 asp0 = ZChain.asupf zc
878 zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → 886 zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u →
879 FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) 887 FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
880 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup 888 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 u≤px)) ( ChainP.order is-sup
881 (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where 889 (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 u≤px)) ss<spx) (fcpu fc zc18) ) where
882 zc19 : u o≤ px
883 zc19 = o<→≤ a
884 zc18 : s o≤ px 890 zc18 : s o≤ px
885 zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 891 zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px
886 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) 892 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
887 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) 893 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc )
888 ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) ) 894 ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b )))
889 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) 895 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
890 zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z 896 zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
891 zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ 897 zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
892 zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where 898 zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
893 u<x : u o< x 899 u<px : u o< px
894 u<x = ? 900 u<px = ZChain.supf-inject zc su<sx
901 u<x : u o< x
902 u<x = ordtrans u<px px<x
903 u≤px : u o≤ px
904 u≤px = o<→≤ u<px
905 s1u<s1x : supf1 u o< supf1 x
906 s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) su<sx) (supf1-mono (o<→≤ px<x) )
895 zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1 907 zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1
896 zc21 {z1} (fsuc z2 fc ) with zc21 fc 908 zc21 {z1} (fsuc z2 fc ) with zc21 fc
897 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 909 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
898 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 910 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
899 zc21 (init asp refl ) with trio< u px | inspect supf1 u 911 zc21 (init asp refl ) with trio< u px | inspect supf1 u
900 ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u 912 ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u
901 ? 913 s1u<s1x
902 record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) } zc14 ⟫ where 914 record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (ChainP.supu=u is-sup) } zc14 ⟫ where
903 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → 915 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
904 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) 916 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
905 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ ?))) ( ChainP.order is-sup 917 zc17 {s} {z1} ss<su fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<px))) ( ChainP.order is-sup
906 (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ ?)) ss<spx) (fcup fc s≤px) ) where 918 (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<px)) ss<su) (fcup fc s≤px) ) where
907 s≤px : s o≤ px 919 s≤px : s o≤ px -- ss<su : supf1 s o< supf1 u
908 s≤px = ? -- ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x) 920 s≤px = ordtrans ( supf-inject0 supf1-mono ss<su ) (o<→≤ u<px)
909 zc14 : FClosure A f (supf1 u) (supf0 u) 921 zc14 : FClosure A f (supf1 u) (supf0 u)
910 zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?) 922 zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px)
911 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) 923 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
912 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) ( ChainP.fcy<sup is-sup fc ) 924 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 u≤px )) ( ChainP.fcy<sup is-sup fc )
913 ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 925 ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (subst (λ k → supf1 k o< supf1 x) b s1u<s1x) record { fcy<sup = zc13
914 ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where 926 ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where
915 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) 927 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px )
916 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) 928 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc )
917 zc18 : supf1 px ≡ px 929 zc18 : supf1 px ≡ px
918 zc18 = begin 930 zc18 = begin
927 ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where 939 ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where
928 zc19 : supf1 px ≡ supf0 u 940 zc19 : supf1 px ≡ supf0 u
929 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) 941 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
930 s≤px : s o≤ px 942 s≤px : s o≤ px
931 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) 943 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
932 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ? ⟫ ) 944 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ )
933 zc12 {z} (case2 fc) = zc21 fc where 945 zc12 {z} (case2 fc) = zc21 fc where
934 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 946 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
935 zc21 {z1} (fsuc z2 fc ) with zc21 fc 947 zc21 {z1} (fsuc z2 fc ) with zc21 fc
936 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 948 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
937 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 949 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
938 zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) 950 zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
939 ... | case1 sfpx=px = ⟪ asp , ch-is-sup px ? -- (pxo<x op) 951 ... | case1 sfpx=px = ⟪ asp , ch-is-sup px zc18
940 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where 952 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
941 zc15 : supf1 px ≡ px 953 zc15 : supf1 px ≡ px
942 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) 954 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
955 zc18 : supf1 px o< supf1 x
956 zc18 = ?
943 zc14 : FClosure A f (supf1 px) (supf0 px) 957 zc14 : FClosure A f (supf1 px) (supf0 px)
944 zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl) 958 zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl)
945 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) 959 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
946 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) 960 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
947 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → 961 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
1307 --- 1321 ---
1308 1322
1309 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x 1323 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x
1310 SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) x 1324 SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) x
1311 1325
1312 data ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
1313 ( supf : Ordinal → Ordinal ) (z : Ordinal) : Set n where
1314 zchain : (uz : Ordinal ) → odef (UnionCF A f mf ay supf uz) z → ZChainP f mf ay supf z
1315
1316 auzc : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
1317 (supf : Ordinal → Ordinal ) → {x : Ordinal } → ZChainP f mf ay supf x → odef A x
1318 auzc f mf {y} ay supf {x} (zchain uz ucf) = proj1 ucf
1319
1320 zp-uz : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
1321 (supf : Ordinal → Ordinal ) → {x : Ordinal } → ZChainP f mf ay supf x → Ordinal
1322 zp-uz f mf ay supf (zchain uz _) = uz
1323
1324 uzc⊆zc : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
1325 (supf : Ordinal → Ordinal ) → {x : Ordinal } → (zp : ZChainP f mf ay supf x ) → UChain A f mf ay supf (zp-uz f mf ay supf zp) x
1326 uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-init fc ⟫) = ch-init fc
1327 uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-is-sup u u<x is-sup fc ⟫) with ChainP.supu=u is-sup
1328 ... | eq = ch-is-sup u u<x is-sup fc
1329
1330 UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
1331 (supf : Ordinal → Ordinal ) → HOD
1332 UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x }
1333 ; odmax = & A ; <odmax = λ lt → ∈∧P→o< ⟪ auzc f mf ay supf lt , lift true ⟫ }
1334
1335 uzctotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
1336 → ( supf : Ordinal → Ordinal )
1337 → IsTotalOrderSet (UnionZF f mf ay supf )
1338 uzctotal f mf ay supf {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (uz01 ca cb) where
1339 uz01 : {ua ub : Ordinal } → ZChainP f mf ay supf ua → ZChainP f mf ay supf ub
1340 → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua )
1341 uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb)
1342
1343 msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) 1326 msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1344 → (zc : ZChain A f mf ay x ) 1327 → (zc : ZChain A f mf ay x )
1345 → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x) 1328 → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
1346 msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where 1329 msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
1347 ztotal : IsTotalOrderSet (ZChain.chain zc) 1330 ztotal : IsTotalOrderSet (ZChain.chain zc)