---

Step * 1 1 1 1 of Lemma adj-solution-column

.....assertion..... 
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. c : |r|
5. b : Column(n;r)
6. x : ℕn
7. y : ℕ1
8. i : ℕn
9. x@0 : ℕn - 1
10. y1 : ℕn - 1
⊢ ¬(if (y1) < (x)  then y1  else (y1 + 1) = x ∈ ℤ)
BY
{ AutoSplit }

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  c  :  |r|
5.  b  :  Column(n;r)
6.  x  :  \mBbbN{}n
7.  y  :  \mBbbN{}1
8.  i  :  \mBbbN{}n
9.  x@0  :  \mBbbN{}n  -  1
10.  y1  :  \mBbbN{}n  -  1
\mvdash{}  \mneg{}(if  (y1)  <  (x)    then  y1    else  (y1  +  1)  =  x)


By

---

Latex:
AutoSplit

---

Home Index