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

comparison src/zorn.agda @ 884:36a50c66a00d

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 Sun, 02 Oct 2022 10:19:31 +0900
parents b7fb839cdcd0
children d1a850b5d8e4
comparison
equal deleted inserted replaced
883:b7fb839cdcd0 884:36a50c66a00d
889 supf1 z with trio< z px 889 supf1 z with trio< z px
890 ... | tri< a ¬b ¬c = supf0 z 890 ... | tri< a ¬b ¬c = supf0 z
891 ... | tri≈ ¬a b ¬c = px --- supf px ≡ px 891 ... | tri≈ ¬a b ¬c = px --- supf px ≡ px
892 ... | tri> ¬a ¬b c = sp1 --- this may equal or larger then x, and sp1 ≡ supf x, is not included in UniofCF 892 ... | tri> ¬a ¬b c = sp1 --- this may equal or larger then x, and sp1 ≡ supf x, is not included in UniofCF
893 893
894 apx : odef A px
895 apx = subst (λ k → odef A k ) (sym sfpx=px) ( ZChain.asupf zc )
896
894 asupf1 : {z : Ordinal } → odef A (supf1 z ) 897 asupf1 : {z : Ordinal } → odef A (supf1 z )
895 asupf1 {z} with trio< z px 898 asupf1 {z} with trio< z px
896 ... | tri< a ¬b ¬c = ZChain.asupf zc 899 ... | tri< a ¬b ¬c = ZChain.asupf zc
897 ... | tri≈ ¬a b ¬c = subst (λ k → odef A k ) (trans (cong supf0 b) (sym sfpx=px)) ( ZChain.asupf zc ) 900 ... | tri≈ ¬a b ¬c = subst (λ k → odef A k ) (trans (cong supf0 b) (sym sfpx=px)) ( ZChain.asupf zc )
898 ... | tri> ¬a ¬b c = MinSUP.asm sup1 901 ... | tri> ¬a ¬b c = MinSUP.asm sup1
899 902
900 -- ch1x=pchainpx : UnionCF A f mf ay supf1 x ≡ pchainpx
901 -- ch1x=pchainpx = ?
902
903 -- UnionCF A f mf ay supf0 x ⊆ UnionCF A f mf ay supf1 x
904
905 zc16 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z 903 zc16 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z
906 zc16 {z} z<px with trio< z px 904 zc16 {z} z<px with trio< z px
907 ... | tri< a ¬b ¬c = refl 905 ... | tri< a ¬b ¬c = refl
908 ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b)) 906 ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b))
909 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c ) 907 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c )
908
909 ch1x=pchainpx : UnionCF A f mf ay supf1 x ≡ pchainpx
910 ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where
911 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
912 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc
913 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z
914 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc
915 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
916 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
917 zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with trio< u px
918 ... | tri< a ¬b ¬c = case1 ⟪ az , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } fc ⟫ where
919 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
920 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
921 ... | tri≈ ¬a b ¬c = case2 fc
922 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x ⟫ )
923 zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
924 zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
925 zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = ⟪ az , ch-is-sup u
926 (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc ))
927 record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 (o<→≤ u<x)) (ChainP.supu=u is-sup) } (fcpu fc (o<→≤ u<x)) ⟫ where
928 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
929 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc )
930 zc12 {z} (case2 fc) = ⟪ A∋fc px f mf fc , ch-is-sup px (pxo<x op) record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px) }
931 (subst (λ k → FClosure A f k z ) (trans sfpx=px (sym (zc16 o≤-refl ))) fc) ⟫ where
932 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
933 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
910 934
911 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where 935 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
912 field 936 field
913 tsup : MinSUP A (UnionCF A f mf ay supf1 z) 937 tsup : MinSUP A (UnionCF A f mf ay supf1 z)
914 tsup=sup : supf1 z ≡ MinSUP.sup tsup 938 tsup=sup : supf1 z ≡ MinSUP.sup tsup
920 m = ZChain.minsup zc (o<→≤ a) 944 m = ZChain.minsup zc (o<→≤ a)
921 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m 945 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m
922 ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where 946 ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where
923 m = ZChain.minsup zc (o≤-refl0 b) 947 m = ZChain.minsup zc (o≤-refl0 b)
924 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 948 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
925 ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } where 949 ; x<sup = ? ; minsup = ? } ; tsup=sup = ? }
926 950
927 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w 951 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
928 supf-mono1 {z} {w} z≤w with trio< w px 952 supf-mono1 {z} {w} z≤w with trio< w px
929 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w ) 953 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w )
930 ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w 954 ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w