]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/problems/simple.1
d3e9213f04e4800c71a75a37cefba9eaa296dbe7
[fireball-separation.git] / ocaml / problems / simple.1
1 $! simple: C diverges\r
2 D v0 (x. x) (v1 (x. y. y v2)) (x. y. v1 v3)\r
3 C v4 (v1 v5 v2 v1 (x. v1 x v2) (v0 (v1 v3) (v1 v5 v2) (v6 v2 (x. y. v0 (v1 v3)) (v3 v2 (x. v1 v3))))) (v1 (x. y. y v2) (v5 v5) (x. v5) (v0 (v1 v3) (v1 v5 v2)) (x. y. v0 (v1 v3))) (v6 v2 (x. y. v0 (v1 v3)) (v3 v2 (x. v1 v3)) (v7 (v0 (v1 v3) (v1 v5 v2))) (v1 v3)) (v1 (x. y. y v2) (v5 v5) (x. v5) (x. v8) (x. x v2) (x. v1 v5 v2)) (v1 (x. y. y v2) (v5 v5) (x. v5) (x. v8) (x. x v2) (x. v5) (x. y. z. v8))\r
4 \r
5 $! simple: C diverges in pure (1)\r
6 D v0 v1 (x. y. z. v2 (y (v3 v4))) (v5 (x. v6))\r
7 C v7 (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (v5 v8 v0) (x. x (y. v2 (v8 (y v4))) (x (y. v2 (v8 (y v4)))))) (v8 (v3 v4) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4))))))) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4)))))) (v8 (v3 v4) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4))))))))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (v5 v8 v0)) (v0 v1 (v5 v8 (x. y. v6)) (v8 (v3 v4)) (v5 v8)) (x. v6 (y. v2 (v8 (y v4))) (v8 (v3 v4)) (x (v0 x (v5 v8 (y. z. v6)) (v8 (v3 v4)))))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4)) v4) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4)) (x. y. v6))\r
8 \r
9 $! simple: C diverges in pure (2)\r
10 D v0 (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1))) (x. v0 v1 v6 (v7 (v2 v5) (v0 v2)) (y. x v4 (v0 v1)))\r
11 C v8 (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v2 v5 (x. v0 v1 (v0 x) (v3 v4) v0 v1 v4))) (v0 v1 (v0 v2) (v3 v4) v0 (v3 v4) (x. y. v0) (v0 v1 (v0 v2) (v3 v4)) (v2 v5 (v0 v1 (v0 v2) (v3 v4) v0 v1 (v3 v4 (v0 v1)) (v2 (v0 v2 (v0 v1 (v0 v2)) v2))))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1)) (x. y. z. v0 v1 (v0 v2) (v3 z))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1)) (x. y. z. v0 v1 (v0 v2) (v3 z)) (v0 v1 (v0 v2) (v3 v4) v0 v1 (v3 v4 (v0 v1)) (v2 (v0 v2 (v0 v1 (v0 v2)) v2))))\r