Step
*
1
1
2
1
of Lemma
decidable__all_fset
1. [T] : Type
2. eq : EqDecider(T)@i
3. [P] : T ⟶ ℙ
4. p : ∀x:T. Dec(P[x])@i
5. s : fset(T)@i
6. x : T@i
⊢ uiff(P[x];↑isl(p x))
BY
{ ((GenConcl ⌜(p x) = d ∈ Dec(P[x])⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto)⋅ }
Latex:
Latex:
1. [T] : Type
2. eq : EqDecider(T)@i
3. [P] : T {}\mrightarrow{} \mBbbP{}
4. p : \mforall{}x:T. Dec(P[x])@i
5. s : fset(T)@i
6. x : T@i
\mvdash{} uiff(P[x];\muparrow{}isl(p x))
By
Latex:
((GenConcl \mkleeneopen{}(p x) = d\mkleeneclose{}\mcdot{} THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto)\mcdot{}
Home
Index