Nuprl Lemma : l_before_append_iff
∀[T:Type]. ∀A,B:T List. ∀x,y:T. (x before y ∈ A @ B ⇐⇒ x before y ∈ A ∨ x before y ∈ B ∨ ((x ∈ A) ∧ (y ∈ B)))
Proof
Definitions occuring in Statement :
l_before: x before y ∈ l,
l_member: (x ∈ l),
append: as @ bs,
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
universe: Type
Definitions unfolded in proof :
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
so_apply: x[s],
and: P ∧ Q,
or: P ∨ Q,
prop: ℙ,
so_lambda: λ2x.t[x],
member: t ∈ T,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
append: as @ bs,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
guard: {T},
uimplies: b supposing a,
not: ¬A,
false: False,
cand: A c∧ B
Lemmas referenced :
istype-universe,
l_member_wf,
append_wf,
l_before_wf,
iff_wf,
list_wf,
list_induction,
list_ind_nil_lemma,
nil_wf,
or_wf,
null_nil_lemma,
btrue_wf,
member-implies-null-eq-bfalse,
btrue_neq_bfalse,
nil_before,
cons_wf,
list_ind_cons_lemma,
istype-void,
cons_before,
cons_member,
member_append
Rules used in proof :
universeEquality,
instantiate,
dependent_functionElimination,
unionIsType,
productIsType,
because_Cache,
functionIsType,
rename,
independent_functionElimination,
universeIsType,
productEquality,
unionEquality,
hypothesis,
functionEquality,
lambdaEquality_alt,
sqequalRule,
hypothesisEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
thin,
cut,
lambdaFormation_alt,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
isect_memberEquality,
voidElimination,
voidEquality,
lambdaFormation,
independent_pairFormation,
inrFormation,
inlFormation,
cumulativity,
unionElimination,
productElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
inhabitedIsType,
equalityIstype,
isect_memberEquality_alt,
inlFormation_alt,
inrFormation_alt,
promote_hyp
Latex:
\mforall{}[T:Type]
\mforall{}A,B:T List. \mforall{}x,y:T.
(x before y \mmember{} A @ B \mLeftarrow{}{}\mRightarrow{} x before y \mmember{} A \mvee{} x before y \mmember{} B \mvee{} ((x \mmember{} A) \mwedge{} (y \mmember{} B)))
Date html generated:
2019_10_15-AM-10_21_41
Last ObjectModification:
2019_08_05-PM-02_08_48
Theory : list_1
Home
Index