Step
*
1
1
1
1
1
1
of Lemma
simple-swap-test2_wf
.....subterm..... T:t
1:n
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 : ℤ@i
14. in@j : ℤ@i
⊢ 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@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 ℤ
13. in@i : ℤ@i
14. in@j : ℤ@i
⊢ λ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 : ℤ@i
14. in@j : ℤ@i
15. λ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)) 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:
.....subterm..... T:t
1:n
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{}
13. in@i : \mBbbZ{}@i
14. in@j : \mBbbZ{}@i
\mvdash{} 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.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k))
(\mlambda{}out@k.(A-return(array-model(AType))
(((out@i =\msubz{} in@j) \mwedge{}\msubb{} (out@j =\msubz{} in@i))
\mwedge{}\msubb{} ((\mneg{}\msubb{}(k =\msubz{} i))
\mwedge{}\msubb{} (\mneg{}\msubb{}(k =\msubz{} j)) {}\mRightarrow{}\msubb{} (out@k =\msubz{} in@k)))))))))))))
\mmember{} A-map \mBbbB{}
By
Latex:
Assert \mkleeneopen{}\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.(A-bind(array-model(AType))
(A-coerce(array-model(AType))
(A-fetch'(array-model(AType)) k))
(\mlambda{}out@k.(A-return(array-model(AType))
(((out@i =\msubz{} in@j) \mwedge{}\msubb{} (out@j =\msubz{} in@i))
\mwedge{}\msubb{} ((\mneg{}\msubb{}(k =\msubz{} i))
\mwedge{}\msubb{} (\mneg{}\msubb{}(k =\msubz{} j)) {}\mRightarrow{}\msubb{} (out@k =\msubz{} in@k)))))))))))) \mmember{} \mBbbZ{}
{}\mrightarrow{} (A-map \mBbbB{})\mkleeneclose{}\mcdot{}
Home
Index