### Nuprl Lemma : cycle-transitive2

`∀n:ℕ. ∀L:ℕn List.  (∀x∈L.(∀y∈L.∃m:ℕ||L||. ((cycle(L)^m x) = y ∈ ℕn))) supposing no_repeats(ℕn;L)`

Proof

Definitions occuring in Statement :  cycle: `cycle(L)` l_all: `(∀x∈L.P[x])` no_repeats: `no_repeats(T;l)` length: `||as||` list: `T List` fun_exp: `f^n` int_seg: `{i..j-}` nat: `ℕ` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat: `ℕ` implies: `P `` Q` so_lambda: `λ2x.t[x]` prop: `ℙ` subtype_rel: `A ⊆r B` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` cand: `A c∧ B` int_seg: `{i..j-}` sq_type: `SQType(T)` guard: `{T}` lelt: `i ≤ j < k`
Lemmas referenced :  no_repeats_witness int_seg_wf l_all_iff l_member_wf l_all_wf exists_wf length_wf equal_wf fun_exp_wf int_seg_subtype_nat false_wf cycle_wf subtype_base_sq set_subtype_base lelt_wf int_subtype_base cycle-transitive no_repeats_wf list_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis independent_functionElimination because_Cache dependent_functionElimination sqequalRule lambdaEquality applyEquality independent_isectElimination independent_pairFormation setEquality productElimination instantiate cumulativity intEquality equalityTransitivity equalitySymmetry dependent_set_memberEquality

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}L:\mBbbN{}n  List.    (\mforall{}x\mmember{}L.(\mforall{}y\mmember{}L.\mexists{}m:\mBbbN{}||L||.  ((cycle(L)\^{}m  x)  =  y)))  supposing  no\_repeats(\mBbbN{}n;L)

Date html generated: 2016_05_14-PM-02_27_25
Last ObjectModification: 2015_12_26-PM-04_23_56

Theory : list_1

Home Index