Step
*
1
1
of Lemma
simple-swap-test2_wf
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. k : ℕn
7. A-fetch'(array-model(AType)) i ∈ A-map'(array-model(AType)) ℤ
8. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map ℤ
9. A-fetch'(array-model(AType)) j ∈ A-map'(array-model(AType)) ℤ
10. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
11. A-fetch'(array-model(AType)) k ∈ A-map'(array-model(AType)) ℤ
12. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
⊢ 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 𝔹
BY
{ Assert ⌜λ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 𝔹)⌝⋅ }
1
.....assertion.....
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. k : ℕn
7. A-fetch'(array-model(AType)) i ∈ A-map'(array-model(AType)) ℤ
8. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map ℤ
9. A-fetch'(array-model(AType)) j ∈ A-map'(array-model(AType)) ℤ
10. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
11. A-fetch'(array-model(AType)) k ∈ A-map'(array-model(AType)) ℤ
12. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
⊢ λ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 𝔹)
2
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. k : ℕn
7. A-fetch'(array-model(AType)) i ∈ A-map'(array-model(AType)) ℤ
8. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map ℤ
9. A-fetch'(array-model(AType)) j ∈ A-map'(array-model(AType)) ℤ
10. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
11. A-fetch'(array-model(AType)) k ∈ A-map'(array-model(AType)) ℤ
12. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
13. λ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 𝔹)
⊢ 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:
1. n : \mBbbN{}
2. AType : array\{i:l\}(\mBbbZ{};n)
3. prog : A-map Unit
4. i : \mBbbN{}n
5. j : \mBbbN{}n
6. k : \mBbbN{}n
7. A-fetch'(array-model(AType)) i \mmember{} A-map'(array-model(AType)) \mBbbZ{}
8. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) \mmember{} A-map \mBbbZ{}
9. A-fetch'(array-model(AType)) j \mmember{} A-map'(array-model(AType)) \mBbbZ{}
10. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) \mmember{} A-map \mBbbZ{}
11. A-fetch'(array-model(AType)) k \mmember{} A-map'(array-model(AType)) \mBbbZ{}
12. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) \mmember{} A-map \mBbbZ{}
\mvdash{} A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))
(\mlambda{}in@i.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(\mlambda{}in@j.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k))
(\mlambda{}in@k.(A-bind(array-model(AType)) prog
(\mlambda{}x.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))
(\mlambda{}out@i.(A-bind(array-model(AType))
(A-coerce(array-model(AType))
(A-fetch'(array-model(AType)) j))
(\mlambda{}out@j....))))))))))) \mmember{} A-map \mBbbB{}
By
Latex:
Assert
\mkleeneopen{}\mlambda{}in@i.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(\mlambda{}in@j.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k))
(\mlambda{}in@k.(A-bind(array-model(AType)) prog
(\mlambda{}x.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))
(\mlambda{}out@i....)))))))) \mmember{} \mBbbZ{} {}\mrightarrow{} (A-map \mBbbB{})\mkleeneclose{}\mcdot{}
Home
Index