Nuprl Lemma : decidable__iseg

`∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) `` (∀L1,L2:T List.  Dec(L1 ≤ L2)))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  decidable_functionality iseg_wf and_wf le_wf length_wf equal_wf list_wf firstn_wf iseg-iff-firstn decidable__and2 decidable__le decidable__equal_list all_wf decidable_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination productElimination isect_memberEquality because_Cache sqequalRule lambdaEquality universeEquality

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L1,L2:T  List.    Dec(L1  \mleq{}  L2)))

Date html generated: 2016_05_14-PM-01_31_32
Last ObjectModification: 2015_12_26-PM-05_24_17

Theory : list_1

Home Index