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

comparison src/zorn.agda @ 1003:b9dfe9bc8412

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, 18 Nov 2022 18:14:41 +0900
parents 19ae0591c6dd
children 5c62c97adac9
comparison
equal deleted inserted replaced
1002:19ae0591c6dd 1003:b9dfe9bc8412
1078 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b 1078 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b
1079 z51 : FClosure A f (supf1 px) w 1079 z51 : FClosure A f (supf1 px) w
1080 z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc 1080 z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
1081 z53 : odef A w 1081 z53 : odef A w
1082 z53 = A∋fc {A} _ f mf fc 1082 z53 = A∋fc {A} _ f mf fc
1083 fc1 : FClosure A f (supf1 px) w
1084 fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym (sf1=sf0 o≤-refl )) ) fc
1085 csupf1 : odef (UnionCF A f mf ay supf1 b) w 1083 csupf1 : odef (UnionCF A f mf ay supf1 b) w
1086 csupf1 with trio< (supf0 px) x 1084 csupf1 with trio< (supf0 px) x
1087 ... | tri< sfpx<x ¬b ¬c = csupf2 where 1085 ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx ? cp1 fc1 ⟫ where
1088 -- supf0 px o< x , supf0 px is member of (UnionCF A f mf ay supf1 x) 1086 spx = supf0 px
1089 csupf2 : odef (UnionCF A f mf ay supf1 b) w 1087 fc1 : FClosure A f (supf1 spx) w
1090 csupf2 with osuc-≡< ((zc-b<x _ sfpx<x) ) 1088 fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) ? ) fc
1091 ... | case1 spx=px = ⟪ z53 , ch-is-sup px (subst (λ k → px o< k ) (sym b=x) px<x) cp1 fc1 ⟫ where 1089 z54 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
1092 -- supf0 px ≡ px 1090 z54 {z} ⟪ az , ch-init fc ⟫ = ZChain.fcy<sup zc o≤-refl fc
1093 order : {s z1 : Ordinal} → supf1 s o< supf1 px → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) 1091 z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = subst (λ k → (z ≡ k) ∨ (z << k ))
1094 order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k ))
1095 (trans (sym (ZChain.supf-is-minsup zc o≤-refl)) (sym (sf1=sf0 o≤-refl)) )
1096 (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx)
1097 o≤-refl (fcup fcs (o<→≤ (supf-inject0 supf1-mono ss<spx)) ) ))
1098 cp1 : ChainP A f mf ay supf1 px
1099 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 o≤-refl))
1100 ( ZChain.fcy<sup zc o≤-refl fc )
1101 ; order = order
1102 ; supu=u = trans (sf1=sf0 o≤-refl) spx=px }
1103 ... | case2 spx<px = ⟪ z53 , ch-is-sup spx ? ? ? ⟫ where
1104 spx = supf0 px
1105 z54 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
1106 z54 {z} ⟪ az , ch-init fc ⟫ = ZChain.fcy<sup zc o≤-refl fc
1107 z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = subst (λ k → (z ≡ k) ∨ (z << k ))
1108 (sym (ZChain.supf-is-minsup zc o≤-refl)) 1092 (sym (ZChain.supf-is-minsup zc o≤-refl))
1109 (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< u<px o≤-refl fc )) where 1093 (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< u<px o≤-refl fc )) where
1110 u<px : u o< px 1094 u<px : u o< px
1111 u<px = ZChain.supf-inject zc ( subst (λ k → k o< supf0 px) (sym (ChainP.supu=u is-sup)) u<b ) 1095 u<px = ZChain.supf-inject zc ( subst (λ k → k o< supf0 px) (sym (ChainP.supu=u is-sup)) u<b )
1112 -- u<b : u o< supf0 px 1096 -- u<b : u o< supf0 px
1113 -- is-sup : ChainP A f mf ay (ZChain.supf zc) u 1097 -- is-sup : ChainP A f mf ay (ZChain.supf zc) u
1114 -- fc : FClosure A f (ZChain.supf zc u) z 1098 -- fc : FClosure A f (ZChain.supf zc u) z
1115 z52 : supf1 (supf0 px) ≡ supf0 px 1099 z52 : supf1 (supf0 px) ≡ supf0 px
1116 z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x) 1100 z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x)
1117 ⟪ record { x≤sup = z54 } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ ) 1101 ⟪ record { x≤sup = z54 } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ )
1118 order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx) 1102 order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
1119 order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 1103 order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k ))
1120 (trans (sym (ZChain.supf-is-minsup zc ? )) (sym ? ) ) 1104 (trans (sym (ZChain.supf-is-minsup zc ? )) (sym ? ) )
1121 (MinSUP.x≤sup (ZChain.minsup zc ?) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 1105 (MinSUP.x≤sup (ZChain.minsup zc ?) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx)
1122 ? (fcup fcs ? ) )) 1106 ? (fcup fcs ? ) ))
1123 cp1 : ChainP A f mf ay supf1 spx 1107 cp1 : ChainP A f mf ay supf1 spx
1124 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 ? )) 1108 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 ? ))
1125 ( ZChain.fcy<sup zc ? fc ) 1109 ( ZChain.fcy<sup zc ? fc )
1126 ; order = order 1110 ; order = order
1127 ; supu=u = ? } 1111 ; supu=u = ? }
1128 ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 1112 ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where
1129 -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case 1113 -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case