Step
*
1
1
of Lemma
simple-swap-test_wf
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. A-fetch'(array-model(AType)) i ∈ A-map'(array-model(AType)) ℤ
7. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map ℤ
8. A-fetch'(array-model(AType)) j ∈ A-map'(array-model(AType)) ℤ
9. 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)) 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 𝔹
BY
{ Assert ⌜λi_in.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λj_in.(A-bind(array-model(AType)) prog
(λx.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))
(λi_out.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λj_out.(A-return(array-model(AType))
((i_out =z j_in) ∧b (j_out =z i_in))))))))))) ∈ ℤ ⟶ (A-map 𝔹)⌝⋅ }
1
.....assertion.....
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. A-fetch'(array-model(AType)) i ∈ A-map'(array-model(AType)) ℤ
7. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map ℤ
8. A-fetch'(array-model(AType)) j ∈ A-map'(array-model(AType)) ℤ
9. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
⊢ λi_in.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λj_in.(A-bind(array-model(AType)) prog
(λx.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))
(λi_out.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λj_out.(A-return(array-model(AType)) ((i_out =z j_in) ∧b (j_out =z i_in))))))))))) ∈ ℤ
⟶ (A-map 𝔹)
2
1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. prog : A-map Unit
4. i : ℕn
5. j : ℕn
6. A-fetch'(array-model(AType)) i ∈ A-map'(array-model(AType)) ℤ
7. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map ℤ
8. A-fetch'(array-model(AType)) j ∈ A-map'(array-model(AType)) ℤ
9. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j) ∈ A-map ℤ
10. λi_in.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λj_in.(A-bind(array-model(AType)) prog
(λx.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))
(λi_out.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λj_out.(A-return(array-model(AType)) ((i_out =z j_in) ∧b (j_out =z i_in))))))))))) ∈ ℤ
⟶ (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)) 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:
1. n : \mBbbN{}
2. AType : array\{i:l\}(\mBbbZ{};n)
3. prog : A-map Unit
4. i : \mBbbN{}n
5. j : \mBbbN{}n
6. A-fetch'(array-model(AType)) i \mmember{} A-map'(array-model(AType)) \mBbbZ{}
7. A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) \mmember{} A-map \mBbbZ{}
8. A-fetch'(array-model(AType)) j \mmember{} A-map'(array-model(AType)) \mBbbZ{}
9. 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)) 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-return(array-model(AType))
((out@i =\msubz{} in@j) \mwedge{}\msubb{} (out@j =\msubz{} in@i)))))))))))) \mmember{} A-map \mBbbB{}
By
Latex:
Assert \mkleeneopen{}\mlambda{}i$_{in}$.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(\mlambda{}j$_{in}$.(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{}i$_{out}$.(A-bind(array-model(AType))
(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(\mlambda{}j$_{out}$.(A-return(array-model(AType))
((i$_{out}$ =\msubz{} j$_{in}\000C$) \mwedge{}\msubb{} (j$_{out}$ =\msubz{} i$_{in}$))))))))))) \mmember{} \mBbbZ{}
{}\mrightarrow{} (A-map \mBbbB{})\mkleeneclose{}\mcdot{}
Home
Index