Step
*
1
2
1
2
2
of Lemma
eqmod-by-orbits
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T} ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits. l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)} List
⊢ Bij(ℕ||filter(λo.(||o|| =z 1);orbits)||;{x:T| (f x) = x ∈ T} ;λi.hd(filter(λo.(||o|| =z 1);orbits)[i]))
BY
{ TACTIC:(RepeatFor 2 (D 0) THEN Reduce 0) }
1
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T} ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits. l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)} List
18. a1 : ℕ||filter(λo.(||o|| =z 1);orbits)||
⊢ ∀a2:ℕ||filter(λo.(||o|| =z 1);orbits)||
((hd(filter(λo.(||o|| =z 1);orbits)[a1]) = hd(filter(λo.(||o|| =z 1);orbits)[a2]) ∈ {x:T| (f x) = x ∈ T} )
⇒ (a1 = a2 ∈ ℕ||filter(λo.(||o|| =z 1);orbits)||))
2
.....wf.....
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T} ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits. l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)} List
⊢ istype(ℕ||filter(λo.(||o|| =z 1);orbits)||)
3
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T} ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits. l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)} List
18. b : {x:T| (f x) = x ∈ T}
⊢ ∃a:ℕ||filter(λo.(||o|| =z 1);orbits)||. (hd(filter(λo.(||o|| =z 1);orbits)[a]) = b ∈ {x:T| (f x) = x ∈ T} )
4
.....wf.....
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T} ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits. l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)} List
⊢ istype({x:T| (f x) = x ∈ T} )
Latex:
Latex:
1. n : \mBbbN{}
2. k : \mBbbN{}
3. p : \mBbbN{}
4. T : Type
5. f : T {}\mrightarrow{} T
6. T \msim{} \mBbbN{}n
7. Inj(T;T;f)
8. \{x:T| (f x) = x\} \msim{} \mBbbN{}k
9. orbits : T List List
10. (\mforall{}o\mmember{}orbits.orbit(T;f;o))
11. \mforall{}a:T. (\mexists{}o\mmember{}orbits. (a \mmember{} o))
12. (\mforall{}o1,o2\mmember{}orbits. l\_disjoint(T;o1;o2))
13. no\_repeats(T List;orbits)
14. n = l\_sum(map(\mlambda{}o.||o||;orbits))
15. (\mforall{}orbit\mmember{}orbits.(||orbit|| = 1) \mvee{} (p | ||orbit||))
16. l\_sum(map(\mlambda{}o.||o||;orbits)) \mequiv{} ||filter(\mlambda{}o.(||o|| =\msubz{} 1);orbits)|| mod p
17. filter(\mlambda{}o.(||o|| =\msubz{} 1);orbits) \mmember{} \{o:T List| (o \mmember{} orbits) \mwedge{} (||o|| = 1)\} List
\mvdash{} Bij(\mBbbN{}||filter(\mlambda{}o.(||o|| =\msubz{} 1);orbits)||;\{x:T| (f x) = x\} ;\mlambda{}i.hd(filter(\mlambda{}o.(||o|| =\msubz{} 1);orbits)[i])\000C)
By
Latex:
TACTIC:(RepeatFor 2 (D 0) THEN Reduce 0)
Home
Index