Nuprl Lemma : decidable__list-closed

[T:Type]. ∀L:T List. ∀f:T ⟶ (T List).  ((∀x,y:T.  Dec(x y ∈ T))  Dec(list-closed(T;L;f)))


Proof




Definitions occuring in Statement :  list-closed: list-closed(T;L;f) list: List decidable: Dec(P) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q list-closed: list-closed(T;L;f) member: t ∈ T so_lambda: λ2x.t[x] prop: so_apply: x[s]
Lemmas referenced :  decidable__l_all l_all_wf l_member_wf decidable__l_member decidable_wf equal_wf list_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule Error :lambdaEquality_alt,  applyEquality setElimination rename hypothesis Error :setIsType,  Error :universeIsType,  independent_functionElimination because_Cache Error :functionIsType,  Error :inhabitedIsType,  instantiate universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}f:T  {}\mrightarrow{}  (T  List).    ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  Dec(list-closed(T;L;f)))



Date html generated: 2019_06_20-PM-01_50_58
Last ObjectModification: 2019_05_13-PM-03_36_46

Theory : list_1


Home Index