Step |
Hyp |
Ref |
Expression |
1 |
|
srngstr.r |
โข ๐
= ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ยท โฉ } โช { โจ ( *๐ โ ndx ) , โ โฉ } ) |
2 |
1
|
srngstr |
โข ๐
Struct โจ 1 , 4 โฉ |
3 |
|
baseid |
โข Base = Slot ( Base โ ndx ) |
4 |
|
snsstp1 |
โข { โจ ( Base โ ndx ) , ๐ต โฉ } โ { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ยท โฉ } |
5 |
|
ssun1 |
โข { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ยท โฉ } โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ยท โฉ } โช { โจ ( *๐ โ ndx ) , โ โฉ } ) |
6 |
5 1
|
sseqtrri |
โข { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ยท โฉ } โ ๐
|
7 |
4 6
|
sstri |
โข { โจ ( Base โ ndx ) , ๐ต โฉ } โ ๐
|
8 |
2 3 7
|
strfv |
โข ( ๐ต โ ๐ โ ๐ต = ( Base โ ๐
) ) |