---

Step * of Lemma row-list-matrix_wf

∀[n,m:ℕ]. ∀[r:RngSig]. ∀[L:|r| List List].
  (row-list-matrix(L) ∈ Matrix(n;m;r)) supposing ((∀i:ℕn. (m ≤ ||L[i]||)) and (n ≤ ||L||))
BY
{ ProveWfLemma }

1
1. n : ℕ
2. m : ℕ
3. r : RngSig
4. L : |r| List List
5. n ≤ ||L||
6. ∀i:ℕn. (m ≤ ||L[i]||)
7. x : ℕn
8. y : ℕm
⊢ y < ||L[x]||

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[r:RngSig].  \mforall{}[L:|r|  List  List].
    (row-list-matrix(L)  \mmember{}  Matrix(n;m;r))  supposing  ((\mforall{}i:\mBbbN{}n.  (m  \mleq{}  ||L[i]||))  and  (n  \mleq{}  ||L||))


By

---

Latex:
ProveWfLemma

---

Home Index