Step
*
1
2
1
2
2
1
of Lemma
satisfies-gcd-reduce-eq-constraints
1. n : ℕ+
2. v : ℤ List
3. ||[1 / v]|| = n ∈ ℤ
4. u : ℤ
5. v2 : ℤ List
6. ||[u / v2]|| = n ∈ ℤ
7. v1 : {L:ℤ List| ||L|| = n ∈ ℤ} List
8. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List
((∀as∈sat.[1 / v] ⋅ as =0)
⇒ (∀as∈v1.[1 / v] ⋅ as =0)
⇒ ((↑isl(gcd-reduce-eq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-eq-constraints(sat;v1)).[1 / v] ⋅ as =0)))
9. sat : {L:ℤ List| ||L|| = n ∈ ℤ} List
10. (∀as∈sat.[1 / v] ⋅ as =0)
11. (∀as∈[[u / v2] / v1].[1 / v] ⋅ as =0)
12. ↑null(v2)
⊢ (↑isl(let s' ⟵ if u=0 then inl [[u / v2] / 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';v1)))
∧ (∀as∈outl(let s' ⟵ if u=0 then inl [[u / v2] / 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';v1)).[1 / v] ⋅ as =0)
BY
{ (DVar `v2'
THEN All Reduce
THEN (Trivial ORELSE Thin (-1))
THEN ((CallByValueReduce 0 THENA Auto) THEN Eliminate ⌜n⌝⋅ THEN DVar `v')⋅) }
1
1. n : ℕ+
2. (||[]|| + 1) = n ∈ ℤ
3. u : ℤ
4. 1 = (||[]|| + 1) ∈ ℤ
5. v1 : {L:ℤ List| ||L|| = (||[]|| + 1) ∈ ℤ} List
6. ∀sat:{L:ℤ List| ||L|| = (||[]|| + 1) ∈ ℤ} List
((∀as∈sat.[1] ⋅ as =0)
⇒ (∀as∈v1.[1] ⋅ as =0)
⇒ ((↑isl(gcd-reduce-eq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-eq-constraints(sat;v1)).[1] ⋅ as =0)))
7. sat : {L:ℤ List| ||L|| = (||[]|| + 1) ∈ ℤ} List
8. (∀as∈sat.[1] ⋅ as =0)
9. (∀as∈[[u] / v1].[1] ⋅ as =0)
⊢ (↑isl(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]);if u=0 then inl [[u] / sat] else (inr ⋅ );v1)))
∧ (∀as∈outl(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]);if u=0 then inl [[u] / sat] else (inr ⋅ );v1)).[1]\000C ⋅ as =0)
2
1. u1 : ℤ
2. v : ℤ List
3. n : ℕ+
4. (||[u1 / v]|| + 1) = n ∈ ℤ
5. u : ℤ
6. 1 = (||[u1 / v]|| + 1) ∈ ℤ
7. v1 : {L:ℤ List| ||L|| = (||[u1 / v]|| + 1) ∈ ℤ} List
8. ∀sat:{L:ℤ List| ||L|| = (||[u1 / v]|| + 1) ∈ ℤ} List
((∀as∈sat.[1; [u1 / v]] ⋅ as =0)
⇒ (∀as∈v1.[1; [u1 / v]] ⋅ as =0)
⇒ ((↑isl(gcd-reduce-eq-constraints(sat;v1)))
∧ (∀as∈outl(gcd-reduce-eq-constraints(sat;v1)).[1; [u1 / v]] ⋅ as =0)))
9. sat : {L:ℤ List| ||L|| = (||[u1 / v]|| + 1) ∈ ℤ} List
10. (∀as∈sat.[1; [u1 / v]] ⋅ as =0)
11. (∀as∈[[u] / v1].[1; [u1 / v]] ⋅ as =0)
⊢ (↑isl(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]);if u=0 then inl [[u] / sat] else (inr ⋅ );v1)))
∧ (∀as∈outl(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]);if u=0 then inl [[u] / sat] else (inr ⋅ );v1)).
[1; [u1 / v]] ⋅ as =0)
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. v : \mBbbZ{} List
3. ||[1 / v]|| = n
4. u : \mBbbZ{}
5. v2 : \mBbbZ{} List
6. ||[u / v2]|| = n
7. v1 : \{L:\mBbbZ{} List| ||L|| = n\} List
8. \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List
((\mforall{}as\mmember{}sat.[1 / v] \mcdot{} as =0)
{}\mRightarrow{} (\mforall{}as\mmember{}v1.[1 / v] \mcdot{} as =0)
{}\mRightarrow{} ((\muparrow{}isl(gcd-reduce-eq-constraints(sat;v1)))
\mwedge{} (\mforall{}as\mmember{}outl(gcd-reduce-eq-constraints(sat;v1)).[1 / v] \mcdot{} as =0)))
9. sat : \{L:\mBbbZ{} List| ||L|| = n\} List
10. (\mforall{}as\mmember{}sat.[1 / v] \mcdot{} as =0)
11. (\mforall{}as\mmember{}[[u / v2] / v1].[1 / v] \mcdot{} as =0)
12. \muparrow{}null(v2)
\mvdash{} (\muparrow{}isl(let s' \mleftarrow{}{} if u=0 then inl [[u / v2] / sat] else (inr \mcdot{} )
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';v1)))
\mwedge{} (\mforall{}as\mmember{}outl(let s' \mleftarrow{}{} if u=0 then inl [[u / v2] / sat] else (inr \mcdot{} )
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';v1)).[1 / v] \mcdot{} as =0)
By
Latex:
(DVar `v2'
THEN All Reduce
THEN (Trivial ORELSE Thin (-1))
THEN ((CallByValueReduce 0 THENA Auto) THEN Eliminate \mkleeneopen{}n\mkleeneclose{}\mcdot{} THEN DVar `v')\mcdot{})
Home
Index