Step
*
1
1
of Lemma
next_wf
1. k : ℤ
2. p : {i:ℤ| k < i} ⟶ 𝔹
3. n : ℤ
4. k < n
5. ↑p[n]
6. (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + (n - k)))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}
⊢ (next i > k s.t. ↑p[i]) ∈ {i:ℤ| k < i ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}
BY
{ (DoSubsume THEN Try (Complete (Auto))) }
Latex:
Latex:
1. k : \mBbbZ{}
2. p : \{i:\mBbbZ{}| k < i\} {}\mrightarrow{} \mBbbB{}
3. n : \mBbbZ{}
4. k < n
5. \muparrow{}p[n]
6. (next i > k s.t. \muparrow{}p[i]) \mmember{} \{i:\mBbbZ{}|
(k < i \mwedge{} (i \mleq{} (k + (n - k)))) \mwedge{} (\muparrow{}p[i]) \mwedge{} (\mforall{}j:\{k + 1..i\msupminus{}\}. (\mneg{}\muparrow{}p[j]))\}
\mvdash{} (next i > k s.t. \muparrow{}p[i]) \mmember{} \{i:\mBbbZ{}| k < i \mwedge{} (\muparrow{}p[i]) \mwedge{} (\mforall{}j:\{k + 1..i\msupminus{}\}. (\mneg{}\muparrow{}p[j]))\}
By
Latex:
(DoSubsume THEN Try (Complete (Auto)))
Home
Index