-lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓c →
- ∃∃ri0,rs0,ti0,ts0. ri0+rs0 = ri & 0 = rs & ti0+ts0 = ti & 0 = ts &
- 〈ri0, rs0, ti0, ts0〉 = c.
+lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri,rs,ti,ts〉 = ↕*c →
+ ∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
+ 〈ri0,rs0,ti0,ts0〉 = c.