The Subformula Tree of a Formula of the First Order Language
Oleg Okhotnikov · 1996
The following propositions are true: (1) For all real numbers x, y, z such that x ≤ y and y < z holds x < z. (2) For all natural numbers m, k holds m + 1 ≤ k iff m < k. (3) For every finite sequence r holds r = r Seg len r. (4) For every natural number n and for every finite sequence r there exists a finite sequence q such that q = r Seg n and q r. (5) For all finite sequences p, q, r such that q r holds p q p r. (6) Let D be a non empty set, and let r be a finite sequence of elements of D, and let r1, r2 be finite sequences, and let k be a natural number. Suppose k + 1 ≤ len r and r1 = r Seg(k + 1) and r2 = r Seg k. Then there exists an element x of D such that r1 = r2 〈x〉. (7) Let D be a non empty set, and let r be a finite sequence of elements of D, and let r1 be a finite sequence. If 1 ≤ len r and r1 = r Seg 1, then there exists an element x of D such that r1 = 〈x〉.