---

Step * of Lemma simple-swap-test2_wf

No Annotations
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:A-map Unit]. ∀[i,j,k:ℕn].
  (simple-swap-test2(array-model(AType);prog;i;j;k) ∈ A-map 𝔹)
BY
{ ProveWfLemma }

1
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. k : ℕn
⊢ A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i)) 
  (λin@i.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j)) 
          (λin@j.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k)) 
                  (λin@k.(A-bind(array-model(AType)) prog 
                          (λx.(A-bind(array-model(AType)) 
                               (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i)) 
                               (λout@i.(A-bind(array-model(AType)) 
                                        (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j)) 
                                        (λout@j.(A-bind(array-model(AType)) 
                                                 (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k)) 
                                                 (λout@k.(A-return(array-model(AType)) 
                                                          (((out@i =z in@j) ∧b (out@j =z in@i))
                                                          ∧b ((¬b(k =z i))
                                                             ∧b (¬b(k =z j)) ⇒b (out@k =z in@k)))))))))))))))))
  ∈ A-map 𝔹

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(\mBbbZ{};n)].  \mforall{}[prog:A-map  Unit].  \mforall{}[i,j,k:\mBbbN{}n].
    (simple-swap-test2(array-model(AType);prog;i;j;k)  \mmember{}  A-map  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index