Nuprl Lemma : pairwise-append
∀[T:Type]
∀L1,L2:T List.
∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L1 @ L2. P[x;y]) ⇐⇒ ((∀x,y∈L1. P[x;y]) ∧ (∀x,y∈L2. P[x;y])) ∧ (∀x∈L1.(∀y∈L2.P[x;y])))
Proof
Definitions occuring in Statement :
pairwise: (∀x,y∈L. P[x; y]),
l_all: (∀x∈L.P[x]),
append: as @ bs,
list: T List,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
prop: ℙ,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
and: P ∧ Q,
so_apply: x[s],
implies: P ⇒ Q,
append: as @ bs,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
true: True
Lemmas referenced :
list_induction,
all_wf,
list_wf,
uall_wf,
iff_wf,
pairwise_wf2,
append_wf,
l_all_wf,
l_member_wf,
list_ind_nil_lemma,
list_ind_cons_lemma,
nil_wf,
pairwise-nil,
l_all_nil,
l_all_wf_nil,
l_all_cons,
cons_wf,
pairwise-cons,
l_all_append
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
thin,
instantiate,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
cumulativity,
hypothesisEquality,
sqequalRule,
lambdaEquality,
hypothesis,
applyEquality,
universeEquality,
functionEquality,
because_Cache,
productEquality,
productElimination,
setElimination,
rename,
setEquality,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
independent_pairFormation,
natural_numberEquality,
addLevel,
impliesFunctionality,
andLevelFunctionality
Latex:
\mforall{}[T:Type]
\mforall{}L1,L2:T List.
\mforall{}[P:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}']
((\mforall{}x,y\mmember{}L1 @ L2. P[x;y])
\mLeftarrow{}{}\mRightarrow{} ((\mforall{}x,y\mmember{}L1. P[x;y]) \mwedge{} (\mforall{}x,y\mmember{}L2. P[x;y])) \mwedge{} (\mforall{}x\mmember{}L1.(\mforall{}y\mmember{}L2.P[x;y])))
Date html generated:
2016_05_14-PM-01_49_55
Last ObjectModification:
2015_12_26-PM-05_37_30
Theory : list_1
Home
Index