YES
Problem:
strict:
f(x) -> x
weak:
a() -> g(a())
Proof:
Arctic Interpretation Processor:
dimension: 4
interpretation:
[0]
[1]
[a] = [1]
[0],
[2 0 0 0]
[0 1 0 0]
[f](x0) = [0 0 1 0]x0
[0 0 0 1] ,
[0 -& -& -&]
[1 -& -& -&]
[g](x0) = [-& 0 -& 0 ]x0
[-& -& -& -&]
orientation:
[2 0 0 0]
[0 1 0 0]
f(x) = [0 0 1 0]x >= x = x
[0 0 0 1]
[0] [0 ]
[1] [1 ]
a() = [1] >= [1 ] = g(a())
[0] [-&]
problem:
strict:
weak:
a() -> g(a())
Qed