Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015) (Proof shortened by AV, 3-Nov-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | efgval.w | |
|
efgval.r | |
||
efgval2.m | |
||
efgval2.t | |
||
efgred.d | |
||
efgred.s | |
||
efgredlem.1 | |
||
efgredlem.2 | |
||
efgredlem.3 | |
||
efgredlem.4 | |
||
efgredlem.5 | |
||
Assertion | efgredlem | |