Step
*
3
1
2
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. 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)))
⊢ ((∀y∈J.¬↑¬bisname(f y)) ∧ (↑isr(inr y )))
∧ (f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K]))
∧ (nameset([x / J]) ⊆r nameset(I))
∧ (∀z:nameset([x / J]). (↑isname(f[x:=fresh-cname(K)] z)))
∧ (f[x:=fresh-cname(K)] ∈ nameset([x / J]) ⟶ nameset([fresh-cname(K) / K]))
∧ (x ∈ nameset([x / J]))
∧ (nameset([x / J]) ⊆r name-morph-domain(f[x:=fresh-cname(K)];I))
BY
{ TACTIC:(Reduce 0 THEN BetterSplitAndConcl THEN Try (Trivial)) }
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
⊢ f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
2
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])
⊢ nameset([x / J]) ⊆r nameset(I)
3
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)
⊢ ∀z:nameset([x / J]). (↑isname(f[x:=fresh-cname(K)] z))
4
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]). (↑isname(f[x:=fresh-cname(K)] z))
⊢ f[x:=fresh-cname(K)] ∈ nameset([x / J]) ⟶ nameset([fresh-cname(K) / K])
5
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]). (↑isname(f[x:=fresh-cname(K)] z))
16. f[x:=fresh-cname(K)] ∈ nameset([x / J]) ⟶ nameset([fresh-cname(K) / K])
⊢ x ∈ nameset([x / J])
6
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]). (↑isname(f[x:=fresh-cname(K)] z))
16. f[x:=fresh-cname(K)] ∈ nameset([x / J]) ⟶ nameset([fresh-cname(K) / K])
17. x ∈ nameset([x / J])
⊢ nameset([x / J]) ⊆r name-morph-domain(f[x:=fresh-cname(K)];I)
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 )
\mvdash{} ((\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f y)) \mwedge{} (\muparrow{}isr(inr y )))
\mwedge{} (f[x:=fresh-cname(K)] \mmember{} name-morph(I;[fresh-cname(K) / K]))
\mwedge{} (nameset([x / J]) \msubseteq{}r nameset(I))
\mwedge{} (\mforall{}z:nameset([x / J]). (\muparrow{}isname(f[x:=fresh-cname(K)] z)))
\mwedge{} (f[x:=fresh-cname(K)] \mmember{} nameset([x / J]) {}\mrightarrow{} nameset([fresh-cname(K) / K]))
\mwedge{} (x \mmember{} nameset([x / J]))
\mwedge{} (nameset([x / J]) \msubseteq{}r name-morph-domain(f[x:=fresh-cname(K)];I))
By
Latex:
TACTIC:(Reduce 0 THEN BetterSplitAndConcl THEN Try (Trivial))
Home
Index