Step
*
2
1
1
2
2
2
of Lemma
satisfies-gcd-reduce-ineq-constraints
1. n : ℕ+
2. xs : {L:ℤ List| ||L|| = n ∈ ℤ}
3. 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ)
4. u : ℤ
5. v1 : ℤ List
6. [%4] : ||[u / v1]|| = n ∈ ℤ
7. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
8. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List
((↑isl(gcd-reduce-ineq-constraints(sat;v)))
⇒ (∀as∈outl(gcd-reduce-ineq-constraints(sat;v)).xs ⋅ as ≥0)
⇒ (∀as∈v.xs ⋅ as ≥0))
9. sat : {L:ℤ List| ||L|| = n ∈ ℤ} List
10. ¬↑null(v1)
⊢ (↑isl(let s' ⟵ eval g = |gcd-list(v1)| in
if (1) < (g)
then eval h' = u ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);v1) in
inl [[h' / t'] / sat]
else (inl [[u / v1] / sat])
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);s';v)))
⇒ (∀as∈outl(let s' ⟵ eval g = |gcd-list(v1)| in
if (1) < (g)
then eval h' = u ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);v1) in
inl [[h' / t'] / sat]
else (inl [[u / v1] / sat])
in accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);s';v)).xs ⋅ as ≥0)
⇒ (∀as∈[[u / v1] / v].xs ⋅ as ≥0)
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)
THEN (((CallByValueReduce 0 THENM Fold `gcd-reduce-ineq-constraints` 0) THENA Auto)
ORELSE ((CallByValueReduceOn ⌜u ÷↓ gg⌝ 0⋅ THENA Auto)
THEN (CallByValueReduceOn ⌜eager-map(λx.(x ÷ gg);v1)⌝ 0⋅ THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN Fold `gcd-reduce-ineq-constraints` 0
THEN (RWO "eager-map-is-map" 0 THENA Auto))
)) }
1
1. n : ℕ+
2. xs : {L:ℤ List| ||L|| = n ∈ ℤ}
3. 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ)
4. u : ℤ
5. v1 : ℤ List
6. ||[u / v1]|| = n ∈ ℤ
7. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
8. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List
((↑isl(gcd-reduce-ineq-constraints(sat;v)))
⇒ (∀as∈outl(gcd-reduce-ineq-constraints(sat;v)).xs ⋅ as ≥0)
⇒ (∀as∈v.xs ⋅ as ≥0))
9. sat : {L:ℤ List| ||L|| = n ∈ ℤ} List
10. ¬↑null(v1)
11. gg : ℤ
12. |gcd-list(v1)| = gg ∈ ℤ
13. 1 < gg
⊢ value-type(ℤ)
2
1. n : ℕ+
2. xs : {L:ℤ List| ||L|| = n ∈ ℤ}
3. 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ)
4. u : ℤ
5. v1 : ℤ List
6. [%4] : ||[u / v1]|| = n ∈ ℤ
7. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
8. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List
((↑isl(gcd-reduce-ineq-constraints(sat;v)))
⇒ (∀as∈outl(gcd-reduce-ineq-constraints(sat;v)).xs ⋅ as ≥0)
⇒ (∀as∈v.xs ⋅ as ≥0))
9. sat : {L:ℤ List| ||L|| = n ∈ ℤ} List
10. ¬↑null(v1)
11. gg : ℤ
12. |gcd-list(v1)| = gg ∈ ℤ
13. 1 < gg
⊢ (↑isl(gcd-reduce-ineq-constraints([[u ÷↓ gg / map(λx.(x ÷ gg);v1)] / sat];v)))
⇒ (∀as∈outl(gcd-reduce-ineq-constraints([[u ÷↓ gg / map(λx.(x ÷ gg);v1)] / sat];v)).xs ⋅ as ≥0)
⇒ (∀as∈[[u / v1] / v].xs ⋅ as ≥0)
3
1. n : ℕ+
2. xs : {L:ℤ List| ||L|| = n ∈ ℤ}
3. 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ)
4. u : ℤ
5. v1 : ℤ List
6. [%4] : ||[u / v1]|| = n ∈ ℤ
7. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
8. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List
((↑isl(gcd-reduce-ineq-constraints(sat;v)))
⇒ (∀as∈outl(gcd-reduce-ineq-constraints(sat;v)).xs ⋅ as ≥0)
⇒ (∀as∈v.xs ⋅ as ≥0))
9. sat : {L:ℤ List| ||L|| = n ∈ ℤ} List
10. ¬↑null(v1)
11. gg : ℤ
12. |gcd-list(v1)| = gg ∈ ℤ
13. ¬1 < gg
⊢ (↑isl(gcd-reduce-ineq-constraints([[u / v1] / sat];v)))
⇒ (∀as∈outl(gcd-reduce-ineq-constraints([[u / v1] / sat];v)).xs ⋅ as ≥0)
⇒ (∀as∈[[u / v1] / v].xs ⋅ as ≥0)
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. xs : \{L:\mBbbZ{} List| ||L|| = n\}
3. 0 < ||xs|| \mwedge{} (hd(xs) = 1)
4. u : \mBbbZ{}
5. v1 : \mBbbZ{} List
6. [\%4] : ||[u / v1]|| = n
7. v : \{L:\mBbbZ{} List| ||L|| = n\} List
8. \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List
((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;v)))
{}\mRightarrow{} (\mforall{}as\mmember{}outl(gcd-reduce-ineq-constraints(sat;v)).xs \mcdot{} as \mgeq{}0)
{}\mRightarrow{} (\mforall{}as\mmember{}v.xs \mcdot{} as \mgeq{}0))
9. sat : \{L:\mBbbZ{} List| ||L|| = n\} List
10. \mneg{}\muparrow{}null(v1)
\mvdash{} (\muparrow{}isl(let s' \mleftarrow{}{} eval g = |gcd-list(v1)| in
if (1) < (g)
then eval h' = u \mdiv{}\mdownarrow{} g in
eval t' = eager-map(\mlambda{}x.(x \mdiv{} g);v1) in
inl [[h' / t'] / sat]
else (inl [[u / v1] / sat])
in accumulate\_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0) then inr \mcdot{} else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h \mdiv{}\mdownarrow{} g in
eval t' = eager-map(\mlambda{}x.(x \mdiv{} g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);s';v)))
{}\mRightarrow{} (\mforall{}as\mmember{}outl(let s' \mleftarrow{}{} eval g = |gcd-list(v1)| in
if (1) < (g)
then eval h' = u \mdiv{}\mdownarrow{} g in
eval t' = eager-map(\mlambda{}x.(x \mdiv{} g);v1) in
inl [[h' / t'] / sat]
else (inl [[u / v1] / sat])
in accumulate\_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0)
then inr \mcdot{}
else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h \mdiv{}\mdownarrow{} g in
eval t' = eager-map(\mlambda{}x.(x \mdiv{} g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);s';v)).xs \mcdot{} as \mgeq{}0)
{}\mRightarrow{} (\mforall{}as\mmember{}[[u / v1] / v].xs \mcdot{} as \mgeq{}0)
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)
THEN (((CallByValueReduce 0 THENM Fold `gcd-reduce-ineq-constraints` 0) THENA Auto)
ORELSE ((CallByValueReduceOn \mkleeneopen{}u \mdiv{}\mdownarrow{} gg\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (CallByValueReduceOn \mkleeneopen{}eager-map(\mlambda{}x.(x \mdiv{} gg);v1)\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN Fold `gcd-reduce-ineq-constraints` 0
THEN (RWO "eager-map-is-map" 0 THENA Auto))
))
Home
Index