Step
*
1
of Lemma
member-gcd-reduce-ineq-constraints
1. n : ℕ+
2. u : {L:ℤ List| ||L|| = n ∈ ℤ}
3. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
4. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-ineq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-ineq-constraints(sat;v))))
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(let s' ⟵ let h,t = u
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [u / sat])
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'] / sat]
else (inl [u / 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)))
⇒ (cc ∈ sat)
⇒ (cc ∈ outl(let s' ⟵ let h,t = u
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [u / sat])
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'] / sat]
else (inl [u / 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))))
BY
{ RepeatFor 2 (DVar `u') }
1
1. n : ℕ+
2. [%2] : ||[]|| = n ∈ ℤ
3. v : {L:ℤ List| ||L|| = n ∈ ℤ} List
4. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-ineq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-ineq-constraints(sat;v))))
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(let s' ⟵ let h,t = []
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [[] / sat])
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'] / sat]
else (inl [[] / 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)))
⇒ (cc ∈ sat)
⇒ (cc ∈ outl(let s' ⟵ let h,t = []
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [[] / sat])
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'] / sat]
else (inl [[] / 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))))
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-ineq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-ineq-constraints(sat;v))))
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(let s' ⟵ let h,t = [u / v1]
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [[u / v1] / sat])
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'] / 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)))
⇒ (cc ∈ sat)
⇒ (cc ∈ outl(let s' ⟵ let h,t = [u / v1]
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [[u / v1] / sat])
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'] / 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))))
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. u : \{L:\mBbbZ{} List| ||L|| = n\}
3. v : \{L:\mBbbZ{} List| ||L|| = n\} List
4. \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List. \mforall{}cc:\{L:\mBbbZ{} List| ||L|| = n\} .
((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;v)))
{}\mRightarrow{} (cc \mmember{} sat)
{}\mRightarrow{} (cc \mmember{} outl(gcd-reduce-ineq-constraints(sat;v))))
\mvdash{} \mforall{}sat:\{L:\mBbbZ{} List| ||L|| = n\} List. \mforall{}cc:\{L:\mBbbZ{} List| ||L|| = n\} .
((\muparrow{}isl(let s' \mleftarrow{}{} let h,t = u
in if t = Ax then if (h) < (0) then inr \mcdot{} else (inl [u / sat])
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'] / sat]
else (inl [u / 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{} (cc \mmember{} sat)
{}\mRightarrow{} (cc \mmember{} outl(let s' \mleftarrow{}{} let h,t = u
in if t = Ax then if (h) < (0) then inr \mcdot{} else (inl [u / sat])
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'] / sat]
else (inl [u / 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))))
By
Latex:
RepeatFor 2 (DVar `u')
Home
Index