Step
*
of Lemma
decidable__list-match-aux
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b]))
⇒ (∀bs:B List. ∀as:A List. ∀used:ℤ List. Dec(list-match-aux(as;bs;used;a,b.R[a;b]))))
BY
{ (RepeatFor 5 ((D 0 THENA Auto)) THEN InductionOnList THEN (D 0 THENA Auto)) }
1
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. ∀a:A. ∀b:B. Dec(R[a;b])
5. bs : B List
6. used : ℤ List
⊢ Dec(list-match-aux([];bs;used;a,b.R[a;b]))
2
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. ∀a:A. ∀b:B. Dec(R[a;b])
5. bs : B List
6. u : A
7. v : A List
8. ∀used:ℤ List. Dec(list-match-aux(v;bs;used;a,b.R[a;b]))
9. used : ℤ List
⊢ Dec(list-match-aux([u / v];bs;used;a,b.R[a;b]))
Latex:
Latex:
\mforall{}[A,B:Type]. \mforall{}[R:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}].
((\mforall{}a:A. \mforall{}b:B. Dec(R[a;b]))
{}\mRightarrow{} (\mforall{}bs:B List. \mforall{}as:A List. \mforall{}used:\mBbbZ{} List. Dec(list-match-aux(as;bs;used;a,b.R[a;b]))))
By
Latex:
(RepeatFor 5 ((D 0 THENA Auto)) THEN InductionOnList THEN (D 0 THENA Auto))
Home
Index