Step
*
1
2
2
of Lemma
member-gcd-reduce-constraints
1. n : ℕ+
2. u : ℤ
3. v1 : ℤ List
4. [%2] : ||[u / v1]|| = n ∈ ℤ
5. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
6. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-eq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-eq-constraints(sat;v))))
7. ¬↑null(v1)
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(let s' ⟵ eval g = |gcd-list(v1)| in
if (1) < (g)
then if u rem g=0
then eval L' = eval x = u ÷ g in
eval r = eager-map(λx.(x ÷ g);v1) in
[x / r] in
inl [L' / sat]
else (inr ⋅ )
else (inl [[u / v1] / sat])
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);s';v)))
⇒ (cc ∈ sat)
⇒ (cc ∈ outl(let s' ⟵ eval g = |gcd-list(v1)| in
if (1) < (g)
then if u rem g=0
then eval L' = eval x = u ÷ g in
eval r = eager-map(λx.(x ÷ g);v1) in
[x / r] in
inl [L' / sat]
else (inr ⋅ )
else (inl [[u / v1] / sat])
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);s';v))))
BY
{ ((GenConcl ⌜|gcd-list(v1)| = gg ∈ ℤ⌝⋅ THENA Auto)
THEN (CallByValueReduceOn ⌜gg⌝ 0⋅ THENA Auto)
THEN (Decide 1 < gg THENA Auto)
THEN (Reduce 0 THENA Auto)) }
1
1. n : ℕ+
2. u : ℤ
3. v1 : ℤ List
4. [%2] : ||[u / v1]|| = n ∈ ℤ
5. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
6. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-eq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-eq-constraints(sat;v))))
7. ¬↑null(v1)
8. gg : ℤ
9. |gcd-list(v1)| = gg ∈ ℤ
10. 1 < gg
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(let s' ⟵ if u rem gg=0
then eval L' = eval x = u ÷ gg in
eval r = eager-map(λx.(x ÷ gg);v1) in
[x / r] in
inl [L' / sat]
else (inr ⋅ )
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);s';v)))
⇒ (cc ∈ sat)
⇒ (cc ∈ outl(let s' ⟵ if u rem gg=0
then eval L' = eval x = u ÷ gg in
eval r = eager-map(λx.(x ÷ gg);v1) in
[x / r] in
inl [L' / sat]
else (inr ⋅ )
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);s';v))))
2
1. n : ℕ+
2. u : ℤ
3. v1 : ℤ List
4. [%2] : ||[u / v1]|| = n ∈ ℤ
5. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
6. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-eq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-eq-constraints(sat;v))))
7. ¬↑null(v1)
8. gg : ℤ
9. |gcd-list(v1)| = gg ∈ ℤ
10. ¬1 < gg
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(let s' ⟵ inl [[u / v1] / sat]
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);s';v)))
⇒ (cc ∈ sat)
⇒ (cc ∈ outl(let s' ⟵ inl [[u / v1] / sat]
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);s';v))))
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. u : \mBbbZ{}
3. v1 : \mBbbZ{} List
4. [\%2] : ||[u / v1]|| = n
5. v : \{L:\mBbbZ{} List| ||L|| = n\} List
6. \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List. \mforall{}cc:\{L:\mBbbZ{} List| ||L|| = n\} .
((\muparrow{}isl(gcd-reduce-eq-constraints(sat;v)))
{}\mRightarrow{} (cc \mmember{} sat)
{}\mRightarrow{} (cc \mmember{} outl(gcd-reduce-eq-constraints(sat;v))))
7. \mneg{}\muparrow{}null(v1)
\mvdash{} \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List. \mforall{}cc:\{L:\mBbbZ{} List| ||L|| = n\} .
((\muparrow{}isl(let s' \mleftarrow{}{} eval g = |gcd-list(v1)| in
if (1) < (g)
then if u rem g=0
then eval L' = eval x = u \mdiv{} g in
eval r = eager-map(\mlambda{}x.(x \mdiv{} g);v1) in
[x / r] in
inl [L' / sat]
else (inr \mcdot{} )
else (inl [[u / v1] / sat])
in accumulate\_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr \mcdot{} )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(\mlambda{}x.(x \mdiv{} g);L) in
inl [L' / Ls]
else (inr \mcdot{} )
else (inl [L / Ls]);s';v)))
{}\mRightarrow{} (cc \mmember{} sat)
{}\mRightarrow{} (cc
\mmember{} outl(let s' \mleftarrow{}{} eval g = |gcd-list(v1)| in
if (1) < (g)
then if u rem g=0
then eval L' = eval x = u \mdiv{} g in
eval r = eager-map(\mlambda{}x.(x \mdiv{} g);v1) in
[x / r] in
inl [L' / sat]
else (inr \mcdot{} )
else (inl [[u / v1] / sat])
in accumulate\_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr \mcdot{} )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(...;L) in
inl [L' / Ls]
else (inr \mcdot{} )
else (inl [L / Ls]);s';v))))
By
Latex:
((GenConcl \mkleeneopen{}|gcd-list(v1)| = gg\mkleeneclose{}\mcdot{} THENA Auto)
THEN (CallByValueReduceOn \mkleeneopen{}gg\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (Decide 1 < gg THENA Auto)
THEN (Reduce 0 THENA Auto))
Home
Index