---

Step * 1 1 2 of Lemma le_witness

.....subterm..... T:t
2:n
1. i : ℤ
2. j : ℤ
3. x1 : ¬less_than'(j;i)
4. x3 : i = i ∈ ℤ
5. x4 : j = j ∈ ℤ
⊢ <Ax, Ax> = <Ax, Ax> ∈ ((i ∈ ℤ) ∧ (j ∈ ℤ))
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  i  :  \mBbbZ{}
2.  j  :  \mBbbZ{}
3.  x1  :  \mneg{}less\_than'(j;i)
4.  x3  :  i  =  i
5.  x4  :  j  =  j
\mvdash{}  <Ax,  Ax>  =  <Ax,  Ax>


By

---

Latex:
Auto

---

Home Index