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

comparison src/zorn.agda @ 906:02f250be89e2

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 Mon, 10 Oct 2022 18:25:04 +0900
parents e6a282eb12fe
children a6f075a164fa
comparison
equal deleted inserted replaced
905:e6a282eb12fe 906:02f250be89e2
1055 m = ZChain.minsup zc (o≤-refl0 b) 1055 m = ZChain.minsup zc (o≤-refl0 b)
1056 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 1056 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
1057 ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } 1057 ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z }
1058 1058
1059 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1059 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1060 csupf1 {z1} sz1<x with trio< (supf1 z1) px 1060 csupf1 {z1} sz1<x = csupf2 where
1061 ... | tri< a ¬b ¬c = csupf0 where 1061 -- z1 o< px → supf1 z1 ≡ supf0 z1
1062 zc18 : supf1 z1 ≡ supf0 z1 1062 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1
1063 zc18 = sf1=sf0 ? 1063 -- z1 ≡ px , supf0 px ≡ px
1064 csupf0 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1064 psz1≤px : supf1 z1 o≤ px
1065 csupf0 with ZChain.csupf zc (subst (λ k → k o< px) zc18 a ) 1065 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x
1066 ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , ch-init ? ⟫ 1066 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1067 ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , 1067 csupf2 with trio< z1 px
1068 ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ? ? ⟫ 1068 csupf2 | tri< a ¬b ¬c with osuc-≡< psz1≤px
1069 ... | tri≈ ¬a b ¬c = ⟪ asm , ch-is-sup (supf1 z1) sz1<x ? (init asm1 ? ) ⟫ where 1069 ... | case1 eq = ? -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
1070 asm : odef A (supf1 z1) 1070 ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
1071 asm = subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 1071 ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) ? ab , ch-init ? ⟫
1072 asm1 : odef A (supf1 (supf1 z1)) 1072 ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? ,
1073 asm1 = subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 1073 ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ? ? ⟫
1074 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) 1074 csupf2 | tri≈ ¬a b ¬c = ? where -- supf1 z1 ≡ supf0 z1, z1 ≡ px
1075 asm : odef A (supf1 z1)
1076 asm = subst (λ k → odef A k ) ? ( MinSUP.asm sup1)
1077 asm1 : odef A (supf1 (supf1 z1))
1078 asm1 = subst (λ k → odef A k ) ? ( MinSUP.asm sup1)
1079 csupf2 | tri> ¬a ¬b c = ?
1075 1080
1076 zc4 : ZChain A f mf ay x --- x o≤ supf px 1081 zc4 : ZChain A f mf ay x --- x o≤ supf px
1077 zc4 with trio< x (supf0 px) 1082 zc4 with trio< x (supf0 px)
1078 ... | tri> ¬a ¬b c = zc41 c 1083 ... | tri> ¬a ¬b c = zc41 c
1079 ... | tri≈ ¬a b ¬c = ? 1084 ... | tri≈ ¬a b ¬c = ?