Page 54 - Textos de Matemática Vol. 40

42 Chapter 1. Applicative theories
Weshowbyinductiononi,thatwehaveforalltermssandallvariantss{m/m}:
s →i k implies CNT ⋆ |= s{m/m} = k.
Afterwards we can choose tm for s and get that CNT ⋆ |= tm = k, and further CNT ⋆ |= tm = tm, because tm is a variant of tm.
Base case. If i = 0, then s is already k.
1.Fork<mthereexistsnopropervariants{m/m}andtheClaimisproven.
2. k = m is impossible by assumption.
3. k > m. Then k is of the form sN (...(sN m)...). Unless s{m/m} is
(k − m)-times
identical to s, it has to be of the form sN (...(sN m)...). By clause (5a)
this term can be reduced to sN (. . . (sN m + 1) . . .) ≡ k.
(k − m − 1)-times
Step case. By induction hypothesis we have for all terms s and variants
s{m/m}:
s→ik implies s{m/m}=k. Wehavetoshowthatforalltermsrandvariantsr{m/m}:
r→i+1k implies r{m/m}=k.
Using the induction hypothesis it is enough to show, that for all r and s with r →1 s and all variants r{m/m} there exists a variant s{m/m} such that r{m/m}=s{m/m}.
By definition of the reduction strategy in CN T ⋆, r →1 s means that there is a subterm r of r which is the first reducible subterm of r, and there is a term s, such that r ρ s holds. We get s by replacing the first occurrence of r in r by s.
First we have to consider that each reduction clause for the pseudo nu- merals has a corresponding one for the numerals, except (5a) So, if r →1 s by rρs,thenthefirstreduciblesubtermofr{m/m}iseitheroftheformsNmor avariantr{m/m}ofr.
LetlbethenumberofoccurrencesofsubtermssNminr{m/m}infront ofthefirstoccurrenceofavariantr{m/m}.Sowegetbylapplicationsofthe reductionclause(5a)thatr{m/m}reducestoanothervariantr′{m/m}whose firstreduciblesubtermisavariantr{m/m}ofr.
Nowwehavetoshowthatwithrρsforallvariantsr{m/m}thereexistsa terms{m/m}suchthatr{m/m}=s{m/m}.Thisisshownbycasedistinction on r ρ s. We only consider proper variants, because the case that r{m/m} is identical with r is trivial.
(k − m)-times