---

Step * 1 1 2 of Lemma eqmod-by-orbits


1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||)) ⇒ (l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p)
⊢ (∀orbit∈[u / v].(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
⇒ ((||u|| + l_sum(map(λo.||o||;v))) ≡ ||if (||u|| =z 1)
   then [u / filter(λo.(||o|| =z 1);v)]
   else filter(λo.(||o|| =z 1);v)
   fi || mod p)
BY
{ ((RWO "l_all_cons" 0 THEN Auto) THEN ThinTrivial THEN SplitOnConclITE THEN Auto) }

1
.....truecase..... 
1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. (||u|| = 1 ∈ ℤ) ∨ (p | ||u||)
6. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
7. l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p
8. ||u|| = 1 ∈ ℤ
⊢ (||u|| + l_sum(map(λo.||o||;v))) ≡ ||[u / filter(λo.(||o|| =z 1);v)]|| mod p

2
.....falsecase..... 
1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. (||u|| = 1 ∈ ℤ) ∨ (p | ||u||)
6. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
7. l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p
8. ¬(||u|| = 1 ∈ ℤ)
⊢ (||u|| + l_sum(map(λo.||o||;v))) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  T  :  Type
3.  u  :  T  List
4.  v  :  T  List  List
5.  (\mforall{}orbit\mmember{}v.(||orbit||  =  1)  \mvee{}  (p  |  ||orbit||))
{}\mRightarrow{}  (l\_sum(map(\mlambda{}o.||o||;v))  \mequiv{}  ||filter(\mlambda{}o.(||o||  =\msubz{}  1);v)||  mod  p)
\mvdash{}  (\mforall{}orbit\mmember{}[u  /  v].(||orbit||  =  1)  \mvee{}  (p  |  ||orbit||))
{}\mRightarrow{}  ((||u||  +  l\_sum(map(\mlambda{}o.||o||;v)))  \mequiv{}  ||if  (||u||  =\msubz{}  1)
      then  [u  /  filter(\mlambda{}o.(||o||  =\msubz{}  1);v)]
      else  filter(\mlambda{}o.(||o||  =\msubz{}  1);v)
      fi  ||  mod  p)


By

---

Latex:
((RWO  "l\_all\_cons"  0  THEN  Auto)  THEN  ThinTrivial  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index