lterms.txt

?- lin_counts(Ks).

counts from 0 to 7
[0,1,0,4,0,27,0,315]

% l=lambda, a=application,-> stands for --o
% both formulas and proof-terms pictured as trees

?- tgo(1).
formula=(0->0)
 ->
  |
 / \
 0  0


proof_term=l(X,X)
  l
  |
 / \
 X  X



true.

?- tgo(2).
true.

?- tgo(3).
formula=(0->(0->1)->1)
   ->
  __|_
 /    \
 0    ->
      _|_
     /   \
    ->    1
     |
    / \
    0  1


proof_term=l(X,l(Y,a(Y,X)))
   l
  _|_
 /   \
 X    l
     _|
    /  \
    Y   a
        |
       / \
       Y  X



formula=((0->0)->0->0)
    ->
   __|_
  /    \
 ->    ->
  |     |
 / \   / \
 0  0  0  0


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=((0->1)->0->1)
    ->
   __|_
  /    \
 ->    ->
  |     |
 / \   / \
 0  1  0  1


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=(((0->0)->0)->0)
      ->
     __|_
    /    \
   ->     0
   _|_
  /   \
 ->    0
  |
 / \
 0  0


proof_term=l(X,a(X,l(Y,Y)))
   l
  _|_
 /   \
 X    a
     _|
    /  \
    X   l
        |
       / \
       Y  Y



true.

?- tgo(4).
true.

?- tgo(5).
formula=(0->1->(1->0->2)->2)
   ->
  __|__
 /     \
 0     ->
     ___|__
    /      \
    1      ->
          __|__
         /     \
        ->      2
        _|
       /  \
       1  ->
           |
          / \
          0  2


proof_term=l(X,l(Y,l(Z,a(a(Z,Y),X))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    X
           |
          / \
          Z  Y



formula=(0->1->(0->1->2)->2)
   ->
  __|__
 /     \
 0     ->
     ___|__
    /      \
    1      ->
          __|__
         /     \
        ->      2
        _|
       /  \
       0  ->
           |
          / \
          1  2


proof_term=l(X,l(Y,l(Z,a(a(Z,X),Y))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Y
           |
          / \
          Z  X



formula=(0->(0->1)->(0->0)->1)
    ->
  ___|__
 /      \
 0      ->
      ___|__
     /      \
    ->      ->
     |      _|_
    / \    /   \
    0  1  ->    1
           |
          / \
          0  0


proof_term=l(X,l(Y,l(Z,a(Y,a(Z,X)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          Y   a
              |
             / \
             Z  X



formula=(0->(1->2)->(0->1)->2)
    ->
  ___|__
 /      \
 0      ->
      ___|__
     /      \
    ->      ->
     |      _|_
    / \    /   \
    1  2  ->    2
           |
          / \
          0  1


proof_term=l(X,l(Y,l(Z,a(Y,a(Z,X)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          Y   a
              |
             / \
             Z  X



formula=(0->(0->1)->(1->2)->2)
    ->
  ___|__
 /      \
 0      ->
      ___|__
     /      \
    ->      ->
     |      _|_
    / \    /   \
    0  1  ->    2
           |
          / \
          1  2


proof_term=l(X,l(Y,l(Z,a(Z,a(Y,X)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          Z   a
              |
             / \
             Y  X



formula=(0->(1->0->2)->1->2)
    ->
  ___|___
 /       \
 0       ->
       ___|__
      /      \
     ->      ->
     _|       |
    /  \     / \
    1  ->    1  2
        |
       / \
       0  2


proof_term=l(X,l(Y,l(Z,a(a(Y,Z),X))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    X
           |
          / \
          Y  Z



formula=(0->(0->1->2)->1->2)
    ->
  ___|___
 /       \
 0       ->
       ___|__
      /      \
     ->      ->
     _|       |
    /  \     / \
    0  ->    1  2
        |
       / \
       1  2


proof_term=l(X,l(Y,l(Z,a(a(Y,X),Z))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Z
           |
          / \
          Y  X



formula=(0->(0->(1->1)->1)->1)
     ->
  ____|___
 /        \
 0        ->
        ___|___
       /       \
      ->        1
     __|_
    /    \
    0    ->
         _|_
        /   \
       ->    1
        |
       / \
       1  1


proof_term=l(X,l(Y,a(a(Y,X),l(Z,Z))))
    l
  __|_
 /    \
 X     l
     __|__
    /     \
    Y      a
         __|_
        /    \
        a     l
        |     |
       / \   / \
       Y  X  Z  Z



formula=((0->1)->0->(0->0)->1)
     ->
   ___|__
  /      \
 ->      ->
  |     __|_
 / \   /    \
 0  1  0    ->
            _|_
           /   \
          ->    1
           |
          / \
          0  0


proof_term=l(X,l(Y,l(Z,a(X,a(Z,Y)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          X   a
              |
             / \
             Z  Y



formula=((0->1)->2->(2->0)->1)
     ->
   ___|__
  /      \
 ->      ->
  |     __|_
 / \   /    \
 0  1  2    ->
            _|_
           /   \
          ->    1
           |
          / \
          2  0


proof_term=l(X,l(Y,l(Z,a(X,a(Z,Y)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          X   a
              |
             / \
             Z  Y



formula=((0->1)->0->(1->2)->2)
     ->
   ___|__
  /      \
 ->      ->
  |     __|_
 / \   /    \
 0  1  0    ->
            _|_
           /   \
          ->    2
           |
          / \
          1  2


proof_term=l(X,l(Y,l(Z,a(Z,a(X,Y)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          Z   a
              |
             / \
             X  Y



formula=((0->1)->(1->2)->0->2)
     ->
   ___|___
  /       \
 ->       ->
  |      __|_
 / \    /    \
 0  1  ->    ->
        |     |
       / \   / \
       1  2  0  2


proof_term=l(X,l(Y,l(Z,a(Y,a(X,Z)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          Y   a
              |
             / \
             X  Z



formula=((0->1)->(2->0)->2->1)
     ->
   ___|___
  /       \
 ->       ->
  |      __|_
 / \    /    \
 0  1  ->    ->
        |     |
       / \   / \
       2  0  2  1


proof_term=l(X,l(Y,l(Z,a(X,a(Y,Z)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          X   a
              |
             / \
             Y  Z



formula=((0->1)->((0->0)->0)->1)
      ->
   ____|____
  /         \
 ->         ->
  |        __|_
 / \      /    \
 0  1    ->     1
         _|_
        /   \
       ->    0
        |
       / \
       0  0


proof_term=l(X,l(Y,a(X,a(Y,l(Z,Z)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       X    a
           _|
          /  \
          Y   l
              |
             / \
             Z  Z



formula=((0->0->0)->0->0->0)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    0  0     0  0


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=((0->1->0)->0->1->0)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  0     1  0


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=((0->0->1)->0->0->1)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    0  1     0  1


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=((0->1->2)->1->0->2)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    1  ->
     |        |
    / \      / \
    1  2     0  2


proof_term=l(X,l(Y,l(Z,a(a(X,Z),Y))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Y
           |
          / \
          X  Z



formula=((0->1->1)->0->1->1)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  1     1  1


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=((0->1->2)->0->1->2)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  2     1  2


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=((0->(1->1)->1)->0->1)
        ->
     ____|___
    /        \
   ->        ->
  __|_        |
 /    \      / \
 0    ->     0  1
      _|_
     /   \
    ->    1
     |
    / \
    1  1


proof_term=l(X,l(Y,a(a(X,Y),l(Z,Z))))
    l
  __|_
 /    \
 X     l
     __|__
    /     \
    Y      a
         __|_
        /    \
        a     l
        |     |
       / \   / \
       X  Y  Z  Z



formula=(((0->0)->0)->(0->0)->0)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    0
  |        |
 / \      / \
 0  0     0  0


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=(((0->1)->0)->(0->1)->0)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    0
  |        |
 / \      / \
 0  1     0  1


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=(((0->0)->1)->(0->0)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    1  ->    1
  |        |
 / \      / \
 0  0     0  0


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=(((0->0)->0)->(0->1)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    1
  |        |
 / \      / \
 0  0     0  1


proof_term=l(X,l(Y,a(Y,a(X,l(Z,Z)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       Y    a
           _|
          /  \
          X   l
              |
             / \
             Z  Z



formula=(((0->1)->1)->(0->1)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    1  ->    1
  |        |
 / \      / \
 0  1     0  1


proof_term=l(X,X)
  l
  |
 / \
 X  X



formula=(((0->1)->2)->(0->1)->2)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    2  ->    2
  |        |
 / \      / \
 0  1     0  1


proof_term=l(X,X)
  l
  |
 / \
 X  X



true.

?- 
formula=((0->1)->(2->0)->2->1)
     ->
   ___|___
  /       \
 ->       ->
  |      __|_
 / \    /    \
 0  1  ->    ->
        |     |
       / \   / \
       2  0  2  1


proof_term=l(A,l(B,l(C,a(A,a(B,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          X   a
              |
             / \
             Y  Z



proof_term=l(A,l(B,l(C,a(A,a(B,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    l
        _|_
       /   \
       Z    a
           _|
          /  \
          X   a
              |
             / \
             Y  Z



formula=((0->1)->((0->0)->0)->1)
      ->
   ____|____
  /         \
 ->         ->
  |        __|_
 / \      /    \
 0  1    ->     1
         _|_
        /   \
       ->    0
        |
       / \
       0  0


proof_term=l(A,l(B,a(A,a(B,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       X    a
           _|
          /  \
          Y   l
              |
             / \
             Z  Z



proof_term=l(A,l(B,a(A,a(B,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       X    a
           _|
          /  \
          Y   l
              |
             / \
             Z  Z



formula=((0->1)->((0->0)->0)->1)
      ->
   ____|____
  /         \
 ->         ->
  |        __|_
 / \      /    \
 0  1    ->     1
         _|_
        /   \
       ->    0
        |
       / \
       0  0


proof_term=l(A,l(B,a(A,a(B,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       X    a
           _|
          /  \
          Y   l
              |
             / \
             Z  Z



proof_term=l(A,l(B,a(A,a(B,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       X    a
           _|
          /  \
          Y   l
              |
             / \
             Z  Z



formula=((0->0->0)->0->0->0)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    0  0     0  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->0->0)->0->0->0)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    0  0     0  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->1->0)->0->1->0)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  0     1  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->1->0)->0->1->0)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  0     1  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->0->1)->0->0->1)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->0->1)->0->0->1)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->1->2)->1->0->2)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    1  ->
     |        |
    / \      / \
    1  2     0  2


proof_term=l(A,l(B,l(C,a(a(A,C),B))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Y
           |
          / \
          X  Z



proof_term=l(A,l(B,l(C,a(a(A,C),B))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Y
           |
          / \
          X  Z



formula=((0->1->2)->1->0->2)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    1  ->
     |        |
    / \      / \
    1  2     0  2


proof_term=l(A,l(B,l(C,a(a(A,C),B))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Y
           |
          / \
          X  Z



proof_term=l(A,l(B,l(C,a(a(A,C),B))))
    l
  __|_
 /    \
 X     l
     __|_
    /    \
    Y     l
        __|_
       /    \
       Z     a
            _|_
           /   \
           a    Y
           |
          / \
          X  Z



formula=((0->1->1)->0->1->1)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  1     1  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->1->1)->0->1->1)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  1     1  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->1->2)->0->1->2)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  2     1  2


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->1->2)->0->1->2)
      ->
    ___|___
   /       \
  ->       ->
  _|       _|
 /  \     /  \
 0  ->    0  ->
     |        |
    / \      / \
    1  2     1  2


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=((0->(1->1)->1)->0->1)
        ->
     ____|___
    /        \
   ->        ->
  __|_        |
 /    \      / \
 0    ->     0  1
      _|_
     /   \
    ->    1
     |
    / \
    1  1


proof_term=l(A,l(B,a(a(A,B),l(C,C))))
    l
  __|_
 /    \
 X     l
     __|__
    /     \
    Y      a
         __|_
        /    \
        a     l
        |     |
       / \   / \
       X  Y  Z  Z



proof_term=l(A,l(B,a(a(A,B),l(C,C))))
    l
  __|_
 /    \
 X     l
     __|__
    /     \
    Y      a
         __|_
        /    \
        a     l
        |     |
       / \   / \
       X  Y  Z  Z



formula=((0->(1->1)->1)->0->1)
        ->
     ____|___
    /        \
   ->        ->
  __|_        |
 /    \      / \
 0    ->     0  1
      _|_
     /   \
    ->    1
     |
    / \
    1  1


proof_term=l(A,l(B,a(a(A,B),l(C,C))))
    l
  __|_
 /    \
 X     l
     __|__
    /     \
    Y      a
         __|_
        /    \
        a     l
        |     |
       / \   / \
       X  Y  Z  Z



proof_term=l(A,l(B,a(a(A,B),l(C,C))))
    l
  __|_
 /    \
 X     l
     __|__
    /     \
    Y      a
         __|_
        /    \
        a     l
        |     |
       / \   / \
       X  Y  Z  Z



formula=(((0->0)->0)->(0->0)->0)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    0
  |        |
 / \      / \
 0  0     0  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->0)->0)->(0->0)->0)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    0
  |        |
 / \      / \
 0  0     0  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->1)->0)->(0->1)->0)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    0
  |        |
 / \      / \
 0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->1)->0)->(0->1)->0)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    0
  |        |
 / \      / \
 0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->0)->1)->(0->0)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    1  ->    1
  |        |
 / \      / \
 0  0     0  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->0)->1)->(0->0)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    1  ->    1
  |        |
 / \      / \
 0  0     0  0


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->0)->0)->(0->1)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    1
  |        |
 / \      / \
 0  0     0  1


proof_term=l(A,l(B,a(B,a(A,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       Y    a
           _|
          /  \
          X   l
              |
             / \
             Z  Z



proof_term=l(A,l(B,a(B,a(A,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       Y    a
           _|
          /  \
          X   l
              |
             / \
             Z  Z



formula=(((0->0)->0)->(0->1)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    0  ->    1
  |        |
 / \      / \
 0  0     0  1


proof_term=l(A,l(B,a(B,a(A,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       Y    a
           _|
          /  \
          X   l
              |
             / \
             Z  Z



proof_term=l(A,l(B,a(B,a(A,l(C,C)))))
   l
  _|_
 /   \
 X    l
     _|_
    /   \
    Y    a
        _|_
       /   \
       Y    a
           _|
          /  \
          X   l
              |
             / \
             Z  Z



formula=(((0->1)->1)->(0->1)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    1  ->    1
  |        |
 / \      / \
 0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->1)->1)->(0->1)->1)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    1  ->    1
  |        |
 / \      / \
 0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->1)->2)->(0->1)->2)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    2  ->    2
  |        |
 / \      / \
 0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



formula=(((0->1)->2)->(0->1)->2)
       ->
     ___|___
    /       \
   ->       ->
   _|_      _|_
  /   \    /   \
 ->    2  ->    2
  |        |
 / \      / \
 0  1     0  1


proof_term=l(A,A)
  l
  |
 / \
 X  X



proof_term=l(A,A)
  l
  |
 / \
 X  X



true.

?-