Step
*
3
1
2
1
3
2
2
of Lemma
cu-filler-cases
1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : nameset(I)
5. f : name-morph(I-[x];K)
6. i : ℕ2
7. box : open_box(c𝕌;I;J;x;i)
8. J ∈ nameset(J) List
9. nameset(J) ⊆r nameset(I-[x])
10. y : (∀y∈J.¬↑¬bisname(f y))
11. l-first(y.¬bisname(f y);J) = (inr y ) ∈ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)))]) ∨ (∀y∈J.¬↑¬bisname(f y)))
12. (∀y∈J.¬↑¬bisname(f y)) ∧ True
13. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
14. nameset([x / J]) ⊆r nameset(I)
15. z : nameset([x / J])
16. ¬(z = x ∈ Cname)
17. z ∈ nameset(I-[x])
⊢ ↑isname(f z)
BY
{ TACTIC:SupposeNot }
1
1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : nameset(I)
5. f : name-morph(I-[x];K)
6. i : ℕ2
7. box : open_box(c𝕌;I;J;x;i)
8. J ∈ nameset(J) List
9. nameset(J) ⊆r nameset(I-[x])
10. y : (∀y∈J.¬↑¬bisname(f y))
11. l-first(y.¬bisname(f y);J) = (inr y ) ∈ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)))]) ∨ (∀y∈J.¬↑¬bisname(f y)))
12. (∀y∈J.¬↑¬bisname(f y)) ∧ True
13. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
14. nameset([x / J]) ⊆r nameset(I)
15. z : nameset([x / J])
16. ¬(z = x ∈ Cname)
17. z ∈ nameset(I-[x])
18. ¬↑isname(f z)
⊢ ↑isname(f z)
Latex:
Latex:
1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : nameset(I)
5. f : name-morph(I-[x];K)
6. i : \mBbbN{}2
7. box : open\_box(c\mBbbU{};I;J;x;i)
8. J \mmember{} nameset(J) List
9. nameset(J) \msubseteq{}r nameset(I-[x])
10. y : (\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f y))
11. l-first(y.\mneg{}\msubb{}isname(f y);J) = (inr y )
12. (\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f y)) \mwedge{} True
13. f[x:=fresh-cname(K)] \mmember{} name-morph(I;[fresh-cname(K) / K])
14. nameset([x / J]) \msubseteq{}r nameset(I)
15. z : nameset([x / J])
16. \mneg{}(z = x)
17. z \mmember{} nameset(I-[x])
\mvdash{} \muparrow{}isname(f z)
By
Latex:
TACTIC:SupposeNot
Home
Index