Step
*
2
1
1
of Lemma
finite-decidable-set
.....assertion.....
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. L : T List@i
5. ∀x:T. (P[x]
⇒ (x ∈ L))
⊢ ∃f:T ⟶ 𝔹. ∀x:T. (↑(f x)
⇐⇒ P[x])
BY
{ TACTIC:(((((Thin (-1))
THEN Unfolds ``all decidable`` 3
THEN RenameVar `f' 3
THEN (InstConcl [⌜λx.case f x of inl(a) => tt | inr(a) => ff⌝])⋅)
THENA Auto
)
THEN Reduce 0
THEN D 0)
THENA Auto
) }
1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. f : x:T ⟶ (P[x] ∨ (¬P[x]))@i
4. L : T List@i
5. x : T@i
⊢ ↑case f x of inl(a) => tt | inr(a) => ff
⇐⇒ P[x]
Latex:
Latex:
.....assertion.....
1. [T] : Type
2. [P] : T {}\mrightarrow{} \mBbbP{}
3. \mforall{}x:T. Dec(P[x])
4. L : T List@i
5. \mforall{}x:T. (P[x] {}\mRightarrow{} (x \mmember{} L))
\mvdash{} \mexists{}f:T {}\mrightarrow{} \mBbbB{}. \mforall{}x:T. (\muparrow{}(f x) \mLeftarrow{}{}\mRightarrow{} P[x])
By
Latex:
TACTIC:(((((Thin (-1))
THEN Unfolds ``all decidable`` 3
THEN RenameVar `f' 3
THEN (InstConcl [\mkleeneopen{}\mlambda{}x.case f x of inl(a) => tt | inr(a) => ff\mkleeneclose{}])\mcdot{})
THENA Auto
)
THEN Reduce 0
THEN D 0)
THENA Auto
)
Home
Index