Step
*
2
of Lemma
fan-implies-bar-sep
1. [T] : Type
2. Fan_d(T)
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. ¬(size = 0 ∈ ℤ)
⊢ tbar(T;A) ∨ tbar(T;B)
BY
{ ((Assert ⌜T⌝⋅ BY (D 4 THEN D 5 THEN With ⌜0⌝ (D 6)⋅ THEN ExRepD THEN Auto)) THEN Thin (-2) THEN PromoteHyp (-1) 3)⋅ }
1
1. [T] : Type
2. Fan_d(T)
3. T
4. size : ℕ
5. T ~ ℕsize
6. A : (T List) ⟶ ℙ
7. B : (T List) ⟶ ℙ
8. Decidable(A)
9. Decidable(B)
10. jbar(T;T;A;B)
⊢ tbar(T;A) ∨ tbar(T;B)
Latex:
Latex:
1. [T] : Type
2. Fan\_d(T)
3. size : \mBbbN{}
4. T \msim{} \mBbbN{}size
5. A : (T List) {}\mrightarrow{} \mBbbP{}
6. B : (T List) {}\mrightarrow{} \mBbbP{}
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. \mneg{}(size = 0)
\mvdash{} tbar(T;A) \mvee{} tbar(T;B)
By
Latex:
((Assert \mkleeneopen{}T\mkleeneclose{}\mcdot{} BY
(D 4 THEN D 5 THEN With \mkleeneopen{}0\mkleeneclose{} (D 6)\mcdot{} THEN ExRepD THEN Auto))
THEN Thin (-2)
THEN PromoteHyp (-1) 3)\mcdot{}
Home
Index