Nuprl Lemma : list-injection

[T:Type]
  ((∀x,y:T.  Dec(x y ∈ T))
   (∀L:T List. ∀f:{x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)} .
        ∀x:{x:T| (x ∈ L)} . ∃m:{1..||L|| 1-}. ((f^m x) x ∈ {x:T| (x ∈ L)} supposing Inj({x:T| (x ∈ L)} ;{x:T| (x ∈\000C L)} ;f)))


Proof




Definitions occuring in Statement :  l_member: (x ∈ l) length: ||as|| list: List fun_exp: f^n inject: Inj(A;B;f) int_seg: {i..j-} decidable: Dec(P) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] add: m natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] uimplies: supposing a member: t ∈ T inject: Inj(A;B;f) prop: so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top less_than: a < b squash: T surject: Surj(A;B;f) sq_stable: SqStable(P) l_member: (x ∈ l) nat: le: A ≤ B cand: c∧ B ge: i ≥ 
Lemmas referenced :  equal_wf l_member_wf finite-injection decidable__equal_set length_wf_nat select_wf list-subtype int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf length_wf set_wf inject_wf list_wf all_wf decidable_wf sq_stable__l_member lelt_wf select_member nat_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality axiomEquality hypothesis extract_by_obid isectElimination setEquality cumulativity applyEquality functionExtensionality setElimination rename dependent_set_memberEquality because_Cache independent_functionElimination equalityTransitivity equalitySymmetry independent_isectElimination productElimination unionElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination functionEquality universeEquality imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}  .
                \mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  \mexists{}m:\{1..||L||  +  1\msupminus{}\}.  ((f\^{}m  x)  =  x)  supposing  Inj(\{x:T|  (x  \mmember{}  L)\}  ;\{x:T|  (x\000C  \mmember{}  L)\}  ;f)))



Date html generated: 2017_04_17-AM-07_47_32
Last ObjectModification: 2017_02_27-PM-04_18_28

Theory : list_1


Home Index