Step
*
1
2
1
2
2
of Lemma
satisfies-gcd-reduce-ineq-constraints
1. n : ℕ+
2. v : ℤ List
3. ||[1 / v]|| = n ∈ ℤ
4. u : ℤ
5. v2 : ℤ List
6. [%5] : ||[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-ineq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-ineq-constraints(sat;v1)).[1 / v] ⋅ as ≥0)))
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List
((∀as∈sat.[1 / v] ⋅ as ≥0)
⇒ (∀as∈[[u / v2] / v1].[1 / v] ⋅ as ≥0)
⇒ ((↑isl(gcd-reduce-ineq-constraints(sat;[[u / v2] / v1])))
∧ (∀as∈outl(gcd-reduce-ineq-constraints(sat;[[u / v2] / v1])).[1 / v] ⋅ as ≥0)))
BY
{ ((UnivCD THENA Auto)
THEN Unfold `gcd-reduce-ineq-constraints` 0
THEN (RWW "accumulate_abort_cons_lemma" 0 THENA Auto)
THEN Reduce 0
THEN (Decide ⌜↑null(v2)⌝⋅ THENA Auto)
THEN RW (SweepDnC IsAxiomC) 0) }
1
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-ineq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-ineq-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 inr ⋅ else (inl [[u / v2] / 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';v1)))
∧ (∀as∈outl(let s' ⟵ if (u) < (0) then inr ⋅ else (inl [[u / v2] / 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';v1)).[1 / v] ⋅ as ≥0)
2
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-ineq-constraints(sat;v1))) ∧ (∀as∈outl(gcd-reduce-ineq-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' ⟵ eval g = |gcd-list(v2)| in
if (1) < (g)
then eval h' = u ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);v2) in
inl [[h' / t'] / sat]
else (inl [[u / v2] / 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';v1)))
∧ (∀as∈outl(let s' ⟵ eval g = |gcd-list(v2)| in
if (1) < (g)
then eval h' = u ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);v2) in
inl [[h' / t'] / sat]
else (inl [[u / v2] / 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';v1)).[1 / 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. [\%5] : ||[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 \mgeq{}0)
{}\mRightarrow{} (\mforall{}as\mmember{}v1.[1 / v] \mcdot{} as \mgeq{}0)
{}\mRightarrow{} ((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;v1)))
\mwedge{} (\mforall{}as\mmember{}outl(gcd-reduce-ineq-constraints(sat;v1)).[1 / v] \mcdot{} as \mgeq{}0)))
\mvdash{} \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List
((\mforall{}as\mmember{}sat.[1 / v] \mcdot{} as \mgeq{}0)
{}\mRightarrow{} (\mforall{}as\mmember{}[[u / v2] / v1].[1 / v] \mcdot{} as \mgeq{}0)
{}\mRightarrow{} ((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;[[u / v2] / v1])))
\mwedge{} (\mforall{}as\mmember{}outl(gcd-reduce-ineq-constraints(sat;[[u / v2] / v1])).[1 / v] \mcdot{} as \mgeq{}0)))
By
Latex:
((UnivCD THENA Auto)
THEN Unfold `gcd-reduce-ineq-constraints` 0
THEN (RWW "accumulate\_abort\_cons\_lemma" 0 THENA Auto)
THEN Reduce 0
THEN (Decide \mkleeneopen{}\muparrow{}null(v2)\mkleeneclose{}\mcdot{} THENA Auto)
THEN RW (SweepDnC IsAxiomC) 0)
Home
Index