Step
*
3
1
2
1
3
2
1
1
1
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. nameset(J) ⊆r nameset(I-[x])
9. y : (∀y∈J.¬↑¬bisname(f y))
10. l-first(y.¬bisname(f y);J) = (inr y ) ∈ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)))]) ∨ (∀y∈J.¬↑¬bisname(f y)))
11. (∀y∈J.¬↑¬bisname(f y))
12. True
13. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
14. nameset([x / J]) ⊆r nameset(I)
15. z : Cname
16. i1 : ℕ
17. i1 < ||J||
18. z = J[i1] ∈ Cname
19. ¬(z = x ∈ Cname)
⊢ J[i1] ∈ nameset(I-[x])
BY
{ TACTIC:(GenConclTerm ⌜J[i1]⌝⋅ THENA Auto) }
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. nameset(J) ⊆r nameset(I-[x])
9. y : (∀y∈J.¬↑¬bisname(f y))
10. l-first(y.¬bisname(f y);J) = (inr y ) ∈ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)))]) ∨ (∀y∈J.¬↑¬bisname(f y)))
11. (∀y∈J.¬↑¬bisname(f y))
12. True
13. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
14. nameset([x / J]) ⊆r nameset(I)
15. z : Cname
16. i1 : ℕ
17. i1 < ||J||
18. z = J[i1] ∈ Cname
19. ¬(z = x ∈ Cname)
20. v : nameset(I)
21. J[i1] = v ∈ nameset(I)
⊢ v ∈ nameset(I-[x])
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. nameset(J) \msubseteq{}r nameset(I-[x])
9. y : (\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f y))
10. l-first(y.\mneg{}\msubb{}isname(f y);J) = (inr y )
11. (\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f y))
12. 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 : Cname
16. i1 : \mBbbN{}
17. i1 < ||J||
18. z = J[i1]
19. \mneg{}(z = x)
\mvdash{} J[i1] \mmember{} nameset(I-[x])
By
Latex:
TACTIC:(GenConclTerm \mkleeneopen{}J[i1]\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index