Nuprl Lemma : word-equiv-equiv
∀[X:Type]. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
Proof
Definitions occuring in Statement :
word-equiv: word-equiv(X;w1;w2),
list: T List,
equiv_rel: EquivRel(T;x,y.E[x; y]),
uall: ∀[x:A]. B[x],
union: left + right,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
equiv_rel: EquivRel(T;x,y.E[x; y]),
and: P ∧ Q,
refl: Refl(T;x,y.E[x; y]),
all: ∀x:A. B[x],
member: t ∈ T,
cand: A c∧ B,
sym: Sym(T;x,y.E[x; y]),
implies: P ⇒ Q,
prop: ℙ,
trans: Trans(T;x,y.E[x; y]),
word-equiv: word-equiv(X;w1;w2),
exists: ∃x:A. B[x],
transitive-reflexive-closure: R^*,
or: P ∨ Q,
subtype_rel: A ⊆r B,
infix_ap: x f y
Lemmas referenced :
list_wf,
word-equiv_wf,
transitive-closure_wf,
word-rel_wf,
transitive-reflexive-closure_wf,
word-rel-confluent,
transitive-reflexive-closure_transitivity
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
independent_pairFormation,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
unionEquality,
cumulativity,
hypothesisEquality,
hypothesis,
because_Cache,
universeEquality,
dependent_pairFormation,
sqequalRule,
inlFormation,
applyEquality,
lambdaEquality,
productEquality,
productElimination,
dependent_functionElimination,
independent_functionElimination,
promote_hyp
Latex:
\mforall{}[X:Type]. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
Date html generated:
2017_01_19-PM-02_49_57
Last ObjectModification:
2017_01_14-PM-05_15_36
Theory : free!groups
Home
Index