Re: Happy Now? (Was: Please be patient)

On 20/12/2024 19:31, Mild Shock wrote:

<https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p>
 /* 3 positive test cases */
 % ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = c*k .
 % ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 7,
% X = c*(c*k*k) .
 % ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .
 /* 2 negative test case */
 % ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.

Hmm, gentzen proves them all:
```
?- prove(pos, []=>(a->a)->(a->a), Ps).
Ps = [impI,init(0)] ;
Ps = [impI,impI,init(0)] ;
Ps = [impI,impI,impE(1),[init(0)],[init(0)]] ;
false.
?- prove(pos, []=>a->((a->b)->b), Ps).
Ps = [impI,impI,impE(0),[init(0)],[init(0)]] ;
false.
?- prove(pos, []=>a->(b->a), Ps).
Ps = [impI,impI,init(1)] ;
false.
?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
false.
```
-Julio