Step |
Hyp |
Ref |
Expression |
1 |
|
signsv.p |
โข โจฃ = ( ๐ โ { - 1 , 0 , 1 } , ๐ โ { - 1 , 0 , 1 } โฆ if ( ๐ = 0 , ๐ , ๐ ) ) |
2 |
|
signsv.w |
โข ๐ = { โจ ( Base โ ndx ) , { - 1 , 0 , 1 } โฉ , โจ ( +g โ ndx ) , โจฃ โฉ } |
3 |
|
signsv.t |
โข ๐ = ( ๐ โ Word โ โฆ ( ๐ โ ( 0 ..^ ( โฏ โ ๐ ) ) โฆ ( ๐ ฮฃg ( ๐ โ ( 0 ... ๐ ) โฆ ( sgn โ ( ๐ โ ๐ ) ) ) ) ) ) |
4 |
|
signsv.v |
โข ๐ = ( ๐ โ Word โ โฆ ฮฃ ๐ โ ( 1 ..^ ( โฏ โ ๐ ) ) if ( ( ( ๐ โ ๐ ) โ ๐ ) โ ( ( ๐ โ ๐ ) โ ( ๐ โ 1 ) ) , 1 , 0 ) ) |
5 |
|
signs.h |
โข ๐ป = ( ( โจโ 0 โโฉ ++ ๐น ) โf โ ( ( ๐น ++ โจโ 0 โโฉ ) โf/c ยท ๐ถ ) ) |
6 |
1 2 3 4 5
|
signshf |
โข ( ( ๐น โ Word โ โง ๐ถ โ โ+ ) โ ๐ป : ( 0 ..^ ( ( โฏ โ ๐น ) + 1 ) ) โถ โ ) |
7 |
|
iswrdi |
โข ( ๐ป : ( 0 ..^ ( ( โฏ โ ๐น ) + 1 ) ) โถ โ โ ๐ป โ Word โ ) |
8 |
6 7
|
syl |
โข ( ( ๐น โ Word โ โง ๐ถ โ โ+ ) โ ๐ป โ Word โ ) |