Nuprl Lemma : firstn_last_mklist_sq
∀[T:Type]. ∀[F:ℕ ⟶ T]. ∀n:ℕ+. (mklist(n;F) ~ firstn(n - 1;mklist(n;F)) @ [last(mklist(n;F))]) supposing T ⊆r Base
Proof
Definitions occuring in Statement :
mklist: mklist(n;f),
firstn: firstn(n;as),
last: last(L),
append: as @ bs,
cons: [a / b],
nil: [],
nat_plus: ℕ+,
nat: ℕ,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
subtract: n - m,
natural_number: $n,
base: Base,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T}
Lemmas referenced :
subtype_base_sq,
list_subtype_base,
firstn_last_mklist,
nat_plus_wf,
nat_wf,
subtype_rel_wf,
base_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
thin,
instantiate,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
because_Cache,
independent_isectElimination,
hypothesis,
dependent_functionElimination,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
sqequalRule,
lambdaEquality,
sqequalAxiom,
functionEquality,
isect_memberEquality,
universeEquality
Latex:
\mforall{}[T:Type]
\mforall{}[F:\mBbbN{} {}\mrightarrow{} T]. \mforall{}n:\mBbbN{}\msupplus{}. (mklist(n;F) \msim{} firstn(n - 1;mklist(n;F)) @ [last(mklist(n;F))])
supposing T \msubseteq{}r Base
Date html generated:
2016_05_14-PM-02_06_25
Last ObjectModification:
2015_12_26-PM-05_08_00
Theory : list_1
Home
Index