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 THEN Auto))) }

1
1. : ℕ
2. LL {L:ℤ List| ||L|| (n 1) ∈ ℤ}  List
3. sat {L:ℤ List| ||L|| (n 1) ∈ ℤ}  List
4. ∀L:ℤ List. (||L|| (n 1) ∈ ℤ ∈ Type)
5. : ℤ
6. u1 : ℤ
7. : ℤ 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