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

comparison src/zorn.agda @ 881:3c2ab35da199

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, 30 Sep 2022 17:35:37 +0900
parents d4839adf694d
children 1a84433ebc1b
comparison
equal deleted inserted replaced
880:d4839adf694d 881:3c2ab35da199
912 ... | tri≈ ¬a b ¬c = refl 912 ... | tri≈ ¬a b ¬c = refl
913 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) 913 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl )
914 ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 lt)) (sym sfpx=px) ( supf-mono z≤w ) 914 ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 lt)) (sym sfpx=px) ( supf-mono z≤w )
915 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px 915 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
916 ... | tri< a ¬b ¬c = zc19 where 916 ... | tri< a ¬b ¬c = zc19 where
917 zc19 : supf0 z o≤ sp1 917 zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
918 zc19 = ? 918 zc21 = ZChain.minsup zc (o<→≤ a)
919 zc23 : odef A sp1
920 zc23 = MinSUP.asm sup1
921 zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
922 zc24 {x₁} ux = MinSUP.x<sup sup1 ?
923 zc19 : supf0 z o≤ sp1
924 zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a))) ( MinSUP.minsup zc21 zc23 zc24 )
919 ... | tri≈ ¬a b ¬c = zc18 where 925 ... | tri≈ ¬a b ¬c = zc18 where
920 zc18 : px o≤ sp1 926 zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
927 zc21 = ZChain.minsup zc (o≤-refl0 b)
928 zc18 : px o≤ sp1 -- supf0 z ≡ px
921 zc18 = ? 929 zc18 = ?
922 ... | tri> ¬a ¬b c = o≤-refl 930 ... | tri> ¬a ¬b c = o≤-refl
923 931
924 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z 932 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z
925 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 933 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
1084 zc30 with osuc-≡< z≤x 1092 zc30 with osuc-≡< z≤x
1085 ... | case1 eq = eq 1093 ... | case1 eq = eq
1086 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) 1094 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
1087 zc32 = ZChain.sup zc o≤-refl 1095 zc32 = ZChain.sup zc o≤-refl
1088 zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) 1096 zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
1089 zc34 ne {w} lt with zc11 P ? 1097 zc34 ne {w} lt with zc11 P ⟪ proj1 lt , ? ⟫
1090 ... | case1 lt = SUP.x<sup zc32 lt 1098 ... | case1 lt = SUP.x<sup zc32 lt
1091 ... | case2 ⟪ spx=px , fc ⟫ = ⊥-elim ( ne spx=px ) 1099 ... | case2 ⟪ spx=px , fc ⟫ = ⊥-elim ( ne spx=px )
1092 zc33 : supf0 z ≡ & (SUP.sup zc32) 1100 zc33 : supf0 z ≡ & (SUP.sup zc32)
1093 zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) 1101 zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl )
1094 zc36 : ¬ (supf0 px ≡ px) → STMP z≤x 1102 zc36 : ¬ (supf0 px ≡ px) → STMP z≤x