Hausaufgaben zu TRS, SRS

1. ergänzen: t[p₁ : = s₁][p₂ : = s₂] = ...
2. Normalformen, Termination, Konfluenz des TRS
   
   
   über Signatur {(0, 0),(1, 0),(¬, 1),(∨, 2),(∧, 2)}

   jeweils Beweis (soweit jetzt möglich, später systematisch) oder Gegenbeispiel (mit Reparaturvorschlag)

3. Die Zug-Relation in Hackenbush auf höchstens binären Bäumen als TRS darstellen. (Signatur, Regeln f. Blau)
4. (auf Papier) unendliche Ableitungen finden für
   1. {f (0, y)→f (y, S(0)), f (S(x), y)→f (x, S(y))}
   2. {f (0, S(x), y)→g(f (0, x, S(y)), f (x, y, S(S(0))))
   3. A(A(F, x), y)→A(A(x, A(F, y)), F)
5. (experimentell) unendliche Ableitungen finden für:
   1. {1000→0001110}, allgemein 10^k→0^k1^k0
   2. {0000→0101, 1001→0100}
   3. {0000→0111, 1001→0010}
   4. {0000→0111, 1011→0110}
6. nachrechnen (Abschnitt 3.1, Alg. 3.2, Ex. 3.3: auf Zahlenfolgen, diese repräsentieren Terme) und beweisen:

   Ikebuchi, Nakano: On Properties of B terms, 2020 https://doi.org/10.23638/LMCS-16(2:8)2020