Nuprl Lemma : insert-combine_wf
∀T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x:T. ∀L:T List. (insert-combine(cmp;f;x;L) ∈ T List)
Proof
Definitions occuring in Statement :
insert-combine: insert-combine(cmp;f;x;l),
comparison: comparison(T),
list: T List,
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
insert-combine: insert-combine(cmp;f;x;l),
uall: ∀[x:A]. B[x],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
has-value: (a)↓,
uimplies: b supposing a,
comparison: comparison(T),
so_apply: x[s1;s2;s3]
Lemmas referenced :
list_ind_wf,
list_wf,
cons_wf,
nil_wf,
value-type-has-value,
int-value-type,
ifthenelse_wf,
eq_int_wf,
lt_int_wf,
comparison_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesisEquality,
because_Cache,
hypothesis,
lambdaEquality,
callbyvalueReduce,
intEquality,
independent_isectElimination,
applyEquality,
setElimination,
rename,
natural_numberEquality,
functionEquality,
dependent_functionElimination,
universeEquality
Latex:
\mforall{}T:Type. \mforall{}cmp:comparison(T). \mforall{}f:T {}\mrightarrow{} T {}\mrightarrow{} T. \mforall{}x:T. \mforall{}L:T List. (insert-combine(cmp;f;x;L) \mmember{} T List)
Date html generated:
2016_05_14-PM-02_40_45
Last ObjectModification:
2015_12_26-PM-02_43_54
Theory : list_1
Home
Index