Step
*
of Lemma
test-squash-simp
∀[B:ℤ ⟶ ℤ ⟶ ℙ]. ∀[A:ℤ ⟶ ℙ].
(↓∃x:ℤ
((↓∃v:ℤ. (↓A[x] ∨ (↓A[v]))) ∧ (↓(∃u:ℤ. (↓((↓B[x;u]) ∧ (↓B[u;u])) ∨ ((↓B[u;x]) ∧ B[x;x]))) ∨ (↓∃n:ℕ. (↓4 ≤ n))))
⇐⇒ ↓∃x:ℤ. ((∃v:ℤ. (A[x] ∨ A[v])) ∧ ((∃u:ℤ. ((B[x;u] ∧ B[u;u]) ∨ (B[u;x] ∧ B[x;x]))) ∨ (∃n:ℕ. (4 ≤ n)))))
BY
{ ((UnivCD THENA Auto) THEN RW (SweepDnC RemoveSquashC) 0 THEN Auto) }
Latex:
Latex:
\mforall{}[B:\mBbbZ{} {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} \mBbbP{}]. \mforall{}[A:\mBbbZ{} {}\mrightarrow{} \mBbbP{}].
(\mdownarrow{}\mexists{}x:\mBbbZ{}
((\mdownarrow{}\mexists{}v:\mBbbZ{}. (\mdownarrow{}A[x] \mvee{} (\mdownarrow{}A[v])))
\mwedge{} (\mdownarrow{}(\mexists{}u:\mBbbZ{}. (\mdownarrow{}((\mdownarrow{}B[x;u]) \mwedge{} (\mdownarrow{}B[u;u])) \mvee{} ((\mdownarrow{}B[u;x]) \mwedge{} B[x;x]))) \mvee{} (\mdownarrow{}\mexists{}n:\mBbbN{}. (\mdownarrow{}4 \mleq{} n))))
\mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}x:\mBbbZ{}
((\mexists{}v:\mBbbZ{}. (A[x] \mvee{} A[v]))
\mwedge{} ((\mexists{}u:\mBbbZ{}. ((B[x;u] \mwedge{} B[u;u]) \mvee{} (B[u;x] \mwedge{} B[x;x]))) \mvee{} (\mexists{}n:\mBbbN{}. (4 \mleq{} n)))))
By
Latex:
((UnivCD THENA Auto) THEN RW (SweepDnC RemoveSquashC) 0 THEN Auto)
Home
Index