Step
*
1
of Lemma
tl_nth_tl
1. n : ℕ
2. L : Top List
3. nth_tl(1;nth_tl(n;L)) ~ nth_tl(1 + n;L)
⊢ tl(nth_tl(n;L)) ~ nth_tl(1;nth_tl(n;L))
BY
{ (GenConcl ⌜nth_tl(n;L) = X ∈ Top⌝⋅ THENA Auto) }
1
1. n : ℕ
2. L : Top List
3. nth_tl(1;nth_tl(n;L)) ~ nth_tl(1 + n;L)
4. X : Top
5. nth_tl(n;L) = X ∈ Top
⊢ tl(X) ~ nth_tl(1;X)
Latex:
Latex:
1. n : \mBbbN{}
2. L : Top List
3. nth\_tl(1;nth\_tl(n;L)) \msim{} nth\_tl(1 + n;L)
\mvdash{} tl(nth\_tl(n;L)) \msim{} nth\_tl(1;nth\_tl(n;L))
By
Latex:
(GenConcl \mkleeneopen{}nth\_tl(n;L) = X\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index