---

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

.....subterm..... T:t
1:n
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 if (y1) < (x)  then y1  else (y1 + 1)=x
  then b[if (x@0) < (i)  then x@0  else (x@0 + 1),0]
  else A[if (x@0) < (i)  then x@0  else (x@0 + 1),if (y1) < (x)  then y1  else (y1 + 1)]
= A[if (x@0) < (i)  then x@0  else (x@0 + 1),if (y1) < (x)  then y1  else (y1 + 1)]
∈ |r|
BY
{ (Assert⌜¬(if (y1) < (x)  then y1  else (y1 + 1) = x ∈ ℤ)⌝⋅ THENM (Reduce 0 THEN Auto)) }

1
.....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 ∈ ℤ)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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{}  if  if  (y1)  <  (x)    then  y1    else  (y1  +  1)=x
    then  b[if  (x@0)  <  (i)    then  x@0    else  (x@0  +  1),0]
    else  A[if  (x@0)  <  (i)    then  x@0    else  (x@0  +  1),if  (y1)  <  (x)    then  y1    else  (y1  +  1)]
=  A[if  (x@0)  <  (i)    then  x@0    else  (x@0  +  1),if  (y1)  <  (x)    then  y1    else  (y1  +  1)]


By

---

Latex:
(Assert\mkleeneopen{}\mneg{}(if  (y1)  <  (x)    then  y1    else  (y1  +  1)  =  x)\mkleeneclose{}\mcdot{}  THENM  (Reduce  0  THEN  Auto))

---

Home Index