1) (⫯f)@(1) = 1
2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k
3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k