5 lines
258 B
Text
5 lines
258 B
Text
definition Sum_weird [forward] : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 :=
|
||
λ f g h n, sorry
|
||
(multi-)patterns:
|
||
?M_1 : ℕ → ℕ, ?M_2 : ℕ → ℕ, ?M_3 : ℕ → ℕ, ?M_4 : ℕ
|
||
{Sum ?M_4 (λ x, ?M_1 (?M_2 (?M_3 x)))}
|