### Nuprl Lemma : length_tl

[A:Type]. ∀[l:A List].  ||tl(l)|| (||l|| 1) ∈ ℤ supposing ||l|| ≥

Proof

Definitions occuring in Statement :  length: ||as|| tl: tl(l) list: List uimplies: supposing a uall: [x:A]. B[x] ge: i ≥  subtract: m natural_number: \$n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: all: x:A. B[x] or: P ∨ Q subtract: m ge: i ≥  le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) true: True not: ¬A implies:  Q false: False cons: [a b] top: Top subtype_rel: A ⊆B
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality hypothesis extract_by_obid natural_numberEquality equalityTransitivity equalitySymmetry Error :universeIsType,  because_Cache universeEquality dependent_functionElimination unionElimination productElimination independent_functionElimination voidElimination promote_hyp hypothesis_subsumption voidEquality applyEquality lambdaEquality intEquality minusEquality addEquality

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].    ||tl(l)||  =  (||l||  -  1)  supposing  ||l||  \mgeq{}  1

Date html generated: 2019_06_20-PM-00_40_04
Last ObjectModification: 2018_09_26-PM-02_12_31

Theory : list_0

Home Index