Page 55 - Textos de Matemática Vol. 40

1.7. N-strictness 43 (1) r ≡ k r 0 r 1 ρ r 0 ≡ s .
Inthiscaseitholdsthefollowing:r{m/m}≡kr0{m/m}r1{m/m}= r0{m/m} ≡ s{m/m}.
(2)–(4) r≡ sr0 r1 r2, r≡ p0 (pr0 r1) and r≡ p1 (pr0 r1) are analogous cases. (5) r ≡ p N ( s N l ) ρ l ≡ s .
We can assume m ≤ l + 1, otherwise there is no proper variant.
(5a) For m < l + 1 the only proper variant is pN (sN ... (sN m)...).
By the reduction clause 5a. we get
r{m/m}→1 pN (sN ...(sN m+1)...)≡pN(sNl) ρ l≡s{m/m}.
(l − m)-times (5b)Form=l+1,r{m/m}isoftheformpNm.Withthereduction
clause 5b. we get pN m →1 l ≡ s{m/m}. (6)–(7) r≡dNr0r1l1l2.
As example we show the case l1 = m, l2 > m. All other cases are analogous. In this case a variant has to be one of the following forms:
(l + 1 − m)-times
1. dNr0{m/m}r1{m/m}ml2,
2. dNr0{m/m}r1{m/m}ml2,
3. dN r0{m/m}r1{m/m}m( sN(...(sN
(l2 − n)-times 4. dN r0{m/m}r1{m/m}m ( sN(...(sN
Using the reduction clause (5a) the cases (3) and (4) become instances of the cases (1) and (2). Using (7) and (7b) we get in both cases r1{m/m} ≡ s{m/m}.
(8)–(9) r≡rNr0r1r2l.
Both possible cases can be treated by the reduction clauses (8a) and (9a) in analogy to dN. ⊣
(l2 − n)-times
m)...)), m)...)).