Step
*
1
of Lemma
first_index_equal
1. T : Type
2. u : T
3. v : T List
4. ∀[L2:T List]. ∀[P,Q:T ⟶ 𝔹].
index-of-first a in v.P[a] ∧b Q[a] = index-of-first a in L2.P[a] ∧b Q[a] ∈ ℤ supposing v agree_on(T;a.↑P[a]) L2
5. u1 : T
6. v1 : T List
7. ∀[P,Q:T ⟶ 𝔹].
index-of-first a in [u / v].P[a] ∧b Q[a] = index-of-first a in v1.P[a] ∧b Q[a] ∈ ℤ
supposing [u / v] agree_on(T;a.↑P[a]) v1
8. P : T ⟶ 𝔹
9. Q : T ⟶ 𝔹
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. ∀i:ℕ||v|| + 1. (((↑P[[u / v][i]]) ∨ (↑P[[u1 / v1][i]])) ⇒ ([u / v][i] = [u1 / v1][i] ∈ T))
⊢ if P[u] ∧b Q[u] then 1
if 0 <z index-of-first a in v.P[a] ∧b Q[a] then index-of-first a in v.P[a] ∧b Q[a] + 1
else 0
fi
= if P[u1] ∧b Q[u1] then 1
if 0 <z index-of-first a in v1.P[a] ∧b Q[a] then index-of-first a in v1.P[a] ∧b Q[a] + 1
else 0
fi
∈ ℤ
BY
{ TACTIC:Subst'
index-of-first a in v.P[a] ∧b Q[a] = index-of-first a in v1.P[a] ∧b Q[a] ∈ ℤ
0 }
1
.....equality.....
1. T : Type
2. u : T
3. v : T List
4. ∀[L2:T List]. ∀[P,Q:T ⟶ 𝔹].
index-of-first a in v.P[a] ∧b Q[a] = index-of-first a in L2.P[a] ∧b Q[a] ∈ ℤ supposing v agree_on(T;a.↑P[a]) L2
5. u1 : T
6. v1 : T List
7. ∀[P,Q:T ⟶ 𝔹].
index-of-first a in [u / v].P[a] ∧b Q[a] = index-of-first a in v1.P[a] ∧b Q[a] ∈ ℤ
supposing [u / v] agree_on(T;a.↑P[a]) v1
8. P : T ⟶ 𝔹
9. Q : T ⟶ 𝔹
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. ∀i:ℕ||v|| + 1. (((↑P[[u / v][i]]) ∨ (↑P[[u1 / v1][i]])) ⇒ ([u / v][i] = [u1 / v1][i] ∈ T))
⊢ index-of-first a in v.P[a] ∧b Q[a] = index-of-first a in v1.P[a] ∧b Q[a] ∈ ℤ
2
1. T : Type
2. u : T
3. v : T List
4. ∀[L2:T List]. ∀[P,Q:T ⟶ 𝔹].
index-of-first a in v.P[a] ∧b Q[a] = index-of-first a in L2.P[a] ∧b Q[a] ∈ ℤ supposing v agree_on(T;a.↑P[a]) L2
5. u1 : T
6. v1 : T List
7. ∀[P,Q:T ⟶ 𝔹].
index-of-first a in [u / v].P[a] ∧b Q[a] = index-of-first a in v1.P[a] ∧b Q[a] ∈ ℤ
supposing [u / v] agree_on(T;a.↑P[a]) v1
8. P : T ⟶ 𝔹
9. Q : T ⟶ 𝔹
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. ∀i:ℕ||v|| + 1. (((↑P[[u / v][i]]) ∨ (↑P[[u1 / v1][i]])) ⇒ ([u / v][i] = [u1 / v1][i] ∈ T))
⊢ if P[u] ∧b Q[u] then 1
if 0 <z index-of-first a in v1.P[a] ∧b Q[a] then index-of-first a in v1.P[a] ∧b Q[a] + 1
else 0
fi
= if P[u1] ∧b Q[u1] then 1
if 0 <z index-of-first a in v1.P[a] ∧b Q[a] then index-of-first a in v1.P[a] ∧b Q[a] + 1
else 0
fi
∈ ℤ
Latex:
Latex:
1. T : Type
2. u : T
3. v : T List
4. \mforall{}[L2:T List]. \mforall{}[P,Q:T {}\mrightarrow{} \mBbbB{}].
index-of-first a in v.P[a] \mwedge{}\msubb{} Q[a] = index-of-first a in L2.P[a] \mwedge{}\msubb{} Q[a]
supposing v agree\_on(T;a.\muparrow{}P[a]) L2
5. u1 : T
6. v1 : T List
7. \mforall{}[P,Q:T {}\mrightarrow{} \mBbbB{}].
index-of-first a in [u / v].P[a] \mwedge{}\msubb{} Q[a] = index-of-first a in v1.P[a] \mwedge{}\msubb{} Q[a]
supposing [u / v] agree\_on(T;a.\muparrow{}P[a]) v1
8. P : T {}\mrightarrow{} \mBbbB{}
9. Q : T {}\mrightarrow{} \mBbbB{}
10. (||v|| + 1) = (||v1|| + 1)
11. \mforall{}i:\mBbbN{}||v|| + 1. (((\muparrow{}P[[u / v][i]]) \mvee{} (\muparrow{}P[[u1 / v1][i]])) {}\mRightarrow{} ([u / v][i] = [u1 / v1][i]))
\mvdash{} if P[u] \mwedge{}\msubb{} Q[u] then 1
if 0 <z index-of-first a in v.P[a] \mwedge{}\msubb{} Q[a] then index-of-first a in v.P[a] \mwedge{}\msubb{} Q[a] + 1
else 0
fi
= if P[u1] \mwedge{}\msubb{} Q[u1] then 1
if 0 <z index-of-first a in v1.P[a] \mwedge{}\msubb{} Q[a] then index-of-first a in v1.P[a] \mwedge{}\msubb{} Q[a] + 1
else 0
fi
By
Latex:
TACTIC:Subst'
index-of-first a in v.P[a] \mwedge{}\msubb{} Q[a] = index-of-first a in v1.P[a] \mwedge{}\msubb{} Q[a]
0
Home
Index