---

Step * 1 of Lemma swap-exists


1. n : ℕ
2. AType : array{i:l}(ℤ;n)
⊢ ∃prog:ℕn ⟶ ℕn ⟶ (A-map Unit). ∀[i,j:ℕn].  alt-swap-spec(AType;n;prog)
BY
{ (TACTIC:InstConcl [⌜λi,j. simple-swap(array-model(AType);i;j)⌝]⋅ THEN Auto) }

1
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. i : ℕn
4. j : ℕn
⊢ alt-swap-spec(AType;n;λi,j. simple-swap(array-model(AType);i;j))

2
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : ℕn ⟶ ℕn ⟶ (A-map Unit)
4. i : ℕn
5. j : ℕn
⊢ istype(alt-swap-spec(AType;n;prog))

---

Latex:

---

Latex:

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


By

---

Latex:
(TACTIC:InstConcl  [\mkleeneopen{}\mlambda{}i,j.  simple-swap(array-model(AType);i;j)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index