Step
*
1
1
1
1
of Lemma
simple-swap-test_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. 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 : ℤ@i
⊢ 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 𝔹
BY
{ Assert ⌜λ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 ℤ
10. i_in : ℤ@i
⊢ λ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 : ℤ@i
11. λ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)) 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 𝔹
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. 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{}
10. i$_{in}$ : \mBbbZ{}@i
\mvdash{} 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$_\mbackslash{}ff\000C7bout}$ =\msubz{} j$_{in}$) \mwedge{}\msubb{} (j$_{out}$ =\msubz{} i$_\mbackslash{}ff\000C7bin}$))))))))))
\mmember{} A-map \mBbbB{}
By
Latex:
Assert \mkleeneopen{}\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