---

Step * of Lemma swap-exists

∀n:ℕ. ∀AType:array{i:l}(ℤ;n).  ∃prog:ℕn ⟶ ℕn ⟶ (A-map Unit). ∀[i,j:ℕn].  alt-swap-spec(AType;n;prog)
BY
{ Auto }

1
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
⊢ ∃prog:ℕn ⟶ ℕn ⟶ (A-map Unit). ∀[i,j:ℕn].  alt-swap-spec(AType;n;prog)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}AType:array\{i:l\}(\mBbbZ{};n).
    \mexists{}prog:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  (A-map  Unit).  \mforall{}[i,j:\mBbbN{}n].    alt-swap-spec(AType;n;prog)


By

---

Latex:
Auto

---

Home Index