### Nuprl Lemma : free-word-inv-append1

`∀[X:Type]. ∀[x:free-word(X)].  (free-word-inv(x) + x = 0 ∈ free-word(X))`

Proof

Definitions occuring in Statement :  free-word-inv: `free-word-inv(w)` free-0: `0` free-append: `w + w'` free-word: `free-word(X)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` free-word: `free-word(X)` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` cand: `A c∧ B` free-word-inv: `free-word-inv(w)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` free-append: `w + w'` guard: `{T}` free-0: `0` nil: `[]` it: `⋅` word-equiv: `word-equiv(X;w1;w2)` exists: `∃x:A. B[x]` and: `P ∧ Q` subtype_rel: `A ⊆r B` quotient: `x,y:A//B[x; y]` squash: `↓T` true: `True` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` so_lambda: `λ2x.t[x]` so_apply: `x[s]` top: `Top` append: `as @ bs` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` transitive-reflexive-closure: `R^*` or: `P ∨ Q` infix_ap: `x f y` word-rel: `word-rel(X;w1;w2)` inverse-letters: `a = -b` sq_type: `SQType(T)` false: `False`
Lemmas referenced :  word-equiv-equiv list_wf word-equiv_wf map_wf equal_wf reverse_wf quotient-member-eq append_wf nil_wf transitive-reflexive-closure_wf word-rel_wf subtype_rel_self equal-wf-base squash_wf true_wf free-word_wf list_induction reverse_nil_lemma map_nil_lemma list_ind_nil_lemma reverse-cons transitive-closure_wf transitive-reflexive-closure_transitivity cons_wf transitive-reflexive-closure-base-case map_append_sq map_cons_lemma inverse-letters_wf length_wf list_ind_cons_lemma length-append exists_wf subtype_base_sq int_subtype_base or_wf append_assoc_sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality unionEquality hypothesis promote_hyp lambdaFormation equalityTransitivity equalitySymmetry because_Cache independent_pairFormation sqequalRule lambdaEquality unionElimination inrEquality inlEquality dependent_functionElimination independent_functionElimination independent_isectElimination dependent_pairFormation productEquality applyEquality instantiate universeEquality pointwiseFunctionality pertypeElimination productElimination imageElimination natural_numberEquality imageMemberEquality baseClosed isect_memberEquality axiomEquality voidElimination voidEquality rename inlFormation applyLambdaEquality inrFormation cumulativity intEquality

Latex:
\mforall{}[X:Type].  \mforall{}[x:free-word(X)].    (free-word-inv(x)  +  x  =  0)

Date html generated: 2020_05_20-AM-08_22_37
Last ObjectModification: 2018_08_21-PM-02_02_22

Theory : free!groups

Home Index