---

Step * of Lemma gcd-reduce-eq-constraints_wf2

∀[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].
  (gcd-reduce-eq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?)
BY
{ (Intros THEN Unhide THEN Unfold `gcd-reduce-eq-constraints` 0 THEN MemCD) }

1
.....implicit subterm..... 
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  ∈ Type

2
.....implicit subterm..... 
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List ∈ Type

3
.....subterm..... T:t
2:n
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ inl sat ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List?

4
.....subterm..... T:t
1:n
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. L : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} 
5. Ls : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ let h,t = L 
  in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ ) otherwise eval g = |gcd-list(t)| in
                                                                     if (1) < (g)
                                                                        then if h rem g=0
                                                                             then eval L' = eager-map(λx.(x ÷ g);L) in
                                                                                  inl [L' / Ls]
                                                                             else (inr ⋅ )
                                                                        else (inl [L / Ls]) ∈ {L:ℤ List| ||L|| = (n + 1)\000C ∈ ℤ}  List?

5
.....wf..... 
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. L : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} 
⊢ istype({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List)

6
.....wf..... 
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ istype({L:ℤ List| ||L|| = (n + 1) ∈ ℤ} )

7
.....subterm..... T:t
3:n
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ LL ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List

8
1. n : ℕ
2. LL : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. sat : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ valueall-type({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[LL,sat:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].
    (gcd-reduce-eq-constraints(sat;LL)  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List?)


By

---

Latex:
(Intros  THEN  Unhide  THEN  Unfold  `gcd-reduce-eq-constraints`  0  THEN  MemCD)

---

Home Index