### Nuprl Lemma : seq-tl-len

`∀[T:Type]. ∀[s:sequence(T)].  ||seq-tl(s)|| ~ ||s|| - 1 supposing 0 < ||s||`

Proof

Definitions occuring in Statement :  seq-tl: `seq-tl(s)` seq-len: `||s||` sequence: `sequence(T)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` subtract: `n - m` natural_number: `\$n` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  guard: `{T}` sq_type: `SQType(T)` true: `True` less_than': `less_than'(a;b)` top: `Top` subtype_rel: `A ⊆r B` subtract: `n - m` uiff: `uiff(P;Q)` prop: `ℙ` false: `False` implies: `P `` Q` rev_implies: `P `` Q` not: `¬A` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` and: `P ∧ Q` le: `A ≤ B` pi1: `fst(t)` seq-tl: `seq-tl(s)` seq-len: `||s||` sequence: `sequence(T)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` nat: `ℕ` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Rules used in proof :  universeEquality sqequalAxiom equalitySymmetry equalityTransitivity minusEquality because_Cache voidEquality isect_memberEquality applyEquality addEquality independent_functionElimination voidElimination lambdaFormation independent_pairFormation unionElimination dependent_functionElimination dependent_set_memberEquality rename setElimination productElimination hypothesisEquality natural_numberEquality lambdaEquality intEquality sqequalRule independent_isectElimination hypothesis cumulativity isectElimination sqequalHypSubstitution extract_by_obid instantiate thin cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].    ||seq-tl(s)||  \msim{}  ||s||  -  1  supposing  0  <  ||s||

Date html generated: 2018_07_25-PM-01_29_15
Last ObjectModification: 2018_06_17-PM-10_09_26

Theory : arithmetic

Home Index