---

Step * of Lemma simple-swap-test_wf

No Annotations
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)].
  let AModel = array-model(AType) in
      ∀[prog:A-map Unit]. ∀[i,j:ℕn].  (simple-swap-test(AModel;prog;i;j) ∈ A-map 𝔹)
BY
{ TACTIC:(ProveWfLemma THEN Unfold `simple-swap-test` 0) }

1
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕ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)) 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-return(array-model(AType)) ((out@i =z in@j) ∧b (out@j =z in@i))))))))))))
  ∈ A-map 𝔹

---

Latex:

---

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


By

---

Latex:
TACTIC:(ProveWfLemma  THEN  Unfold  `simple-swap-test`  0)

---

Home Index