Step
*
of Lemma
gcd-reduce-ineq-constraints_wf2
∀[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].
  (gcd-reduce-ineq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?)
BY
{ (ProveWfLemma THEN Repeat ((CallByValueReduce 0 THEN Auto))) }
1
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. ∀L:ℤ List. (||L|| = (n + 1) ∈ ℤ ∈ Type)
5. u : ℤ
6. u1 : ℤ
7. v : ℤ List
8. ||[u; [u1 / v]]|| = (n + 1) ∈ ℤ
9. Ls : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
10. 1 < |gcd-list([u1 / v])|
⊢ [u ÷↓ |gcd-list([u1 / v])|; [u1 ÷ |gcd-list([u1 / v])| / eager-map(λx.(x ÷ |gcd-list([u1 / v])|);v)]] ∈ {L:ℤ List| 
                                                                                                           ||L||
                                                                                                           = (n + 1)
                                                                                                           ∈ ℤ} 
Latex:
Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[LL,sat:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].
    (gcd-reduce-ineq-constraints(sat;LL)  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List?)
By
Latex:
(ProveWfLemma  THEN  Repeat  ((CallByValueReduce  0  THEN  Auto)))
Home
Index