Nuprl Lemma : singleton-orbit

[T:Type]. ∀[f:T ⟶ T]. ∀[o:T List].  (o ∈ {x:T| (f x) x ∈ T}  List) supposing (orbit(T;f;o) and (||o|| 1 ∈ ℤ))


Proof




Definitions occuring in Statement :  orbit: orbit(T;f;L) length: ||as|| list: List uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] or: P ∨ Q sq_type: SQType(T) implies:  Q guard: {T} true: True false: False cons: [a b] top: Top prop: ge: i ≥  le: A ≤ B and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q nat: less_than': less_than'(a;b) compose: g
Lemmas referenced :  orbit-closed list-cases length_of_nil_lemma subtype_base_sq int_subtype_base product_subtype_list length_of_cons_lemma cons_wf equal_wf non_neg_length satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_formula_prop_wf nil_wf list-set-type2 orbit_wf equal-wf-T-base length_wf list_wf l_all_cons all_wf nat_wf l_member_wf fun_exp_wf false_wf le_wf fun_exp1_lemma member_singleton
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_isectElimination hypothesis unionElimination sqequalRule instantiate cumulativity intEquality equalityTransitivity equalitySymmetry independent_functionElimination natural_numberEquality voidElimination promote_hyp hypothesis_subsumption productElimination isect_memberEquality voidEquality setEquality because_Cache applyEquality functionExtensionality dependent_set_memberEquality rename dependent_pairFormation lambdaEquality int_eqEquality independent_pairFormation computeAll axiomEquality baseClosed functionEquality lambdaFormation

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[o:T  List].
    (o  \mmember{}  \{x:T|  (f  x)  =  x\}    List)  supposing  (orbit(T;f;o)  and  (||o||  =  1))



Date html generated: 2017_04_17-AM-08_14_31
Last ObjectModification: 2017_02_27-PM-04_39_29

Theory : list_1


Home Index