dwolter_SparQ/Calculi/double-cross.lisp
;;; 
;;; Double cross calculus
;;;

(def-calculus "Double Cross Calculus (DCC)"
  :arity :ternary
  :basis-entity :2d-point
  :parametric? nil
  :qualifier (external-lib "libdcc.dylib" "dcc_qualify")
  :identity-relation b_4
  :consistency :unknown
  :inverse-operation (( 0_4 4_0 )
                      ( 7_3 3_7 )
                      ( 6_3 3_6 )
                      ( 5_3 3_5 )
                      ( 5_2 2_5 )
                      ( 5_1 1_5 )
                      ( 4_0 0_4 )
                      ( 3_7 7_3 )
                      ( 3_6 6_3 )
                      ( 3_5 5_3 )
                      ( 2_5 5_2 )
                      ( 1_5 5_1 )
                      ( 4_4 4_4 )
                      ( 4_a b_4 )
                      ( b_4 4_a )
                      ( Dou Dou )
                      ( Tri Tri ))
  
  :shortcut-operation (( 0_4 4_4 )
                       ( 7_3 3_5 )
                       ( 6_3 3_5 )
                       ( 5_3  3_5 2_5 1_5 )
                       ( 5_2 3_6 )
                       ( 5_1 3_7 )
                       ( 4_0 4_0 )
                       ( 3_7 5_1 )
                       ( 3_6 5_2 )
                       ( 3_5  5_3 6_3 7_3 )
                       ( 2_5 5_3 )
                       ( 1_5 5_3 )
                       ( 4_4 0_4 )
                       ( 4_a Dou )
                       ( b_4 b_4 )
                       ( Dou 4_a )
                       ( Tri Tri ))
  
  :homing-operation (( 0_4 4_0 )
                     ( 7_3 5_1 )
                     ( 6_3 5_2 )
                     ( 5_3 5_3 6_3 7_3 )
                     ( 5_2 5_3 )
                     ( 5_1 5_3 )
                     ( 4_0 4_4 )
                     ( 3_7 3_5 )
                     ( 3_6 3_5 )
                     ( 3_5 1_5 2_5 3_5 )
                     ( 2_5 3_6 )
                     ( 1_5 3_7 )
                     ( 4_4 0_4 )
                     ( 4_a b_4 )
                     ( b_4 Dou )
                     ( Dou 4_a )
                     ( Tri Tri ))
  
  :base-relations ( 0_4 7_3 6_3 5_3 5_2 5_1 4_0 3_7 3_6 3_5 2_5 1_5 4_4 4_a b_4 Dou Tri )  
  :algebraic-specification ((Tri ((1 ((ax 1))) = (1 ((bx 1)))) ; a = b
				 ((1 ((ay 1))) = (1 ((by 1))))
				 ((1 ((ax 1))) = (1 ((cx 1)))) ; a = c
				 ((1 ((ay 1))) = (1 ((cy 1)))))
			    (Dou ((1 ((ax 1))) = (1 ((bx 1)))) ; a = b
				 ((1 ((ay 1))) = (1 ((by 1))))
				 (0 < (1 ((ax 2))) (-2 ((ax 1) (cx 1))) (1 ((cx 2))) (1 ((ay 2))) (-2 ((ay 1) (cy 1))) (1 ((cy 2)))))
			    (0_4   (0 < ( 1 ((bx 1)(cx 1))) (-1 ((ax 1)(cx 1))) (1 ((ax 1)(bx 1))) (-1 ((bx 2)))
				      ( 1 ((by 1)(cy 1))) (-1 ((ay 1)(cy 1))) (1 ((ay 1)(by 1))) (-1 ((by 2))))
				   ;;(0 < ( 1 ((bx 1)(cx 1))) (-1 ((bx 1)(ax 1))) (-1 ((ax 1)(cx 1))) (1 ((ax 2)))
				   ;; ( 1 ((by 1)(cy 1))) (-1 ((ay 1)(by 1))) (-1 ((ay 1)(cy 1))) ( 1 ((ay 2))))
				   (0 = (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				      (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1)))))
			    (4_0  (0 > ( 1 ((bx 1)(cx 1))) (-1 ((bx 1)(ax 1))) (-1 ((ax 1)(cx 1))) ( 1 ((ax 2)))
				     ( 1 ((by 1)(cy 1))) (-1 ((ay 1)(by 1))) (-1 ((ay 1)(cy 1))) ( 1 ((ay 2))))
				  ;;(0 > ( 1 ((bx 1)(cx 1))) (-1 ((ax 1)(cx 1))) ( 1 ((ax 1)(bx 1))) (-1 ((bx 2)))
				  ;; ( 1 ((by 1)(cy 1))) (-1 ((ay 1)(cy 1))) ( 1 ((ay 1)(by 1))) (-1 ((by 2))))
				  (0 = (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1)))))
			    (4_4  (0 > ( 1 ((bx 1)(cx 1))) (-1 ((ax 1)(cx 1))) ( 1 ((ax 1)(bx 1))) (-1 ((bx 2)))
				     ( 1 ((by 1)(cy 1))) (-1 ((ay 1)(cy 1))) ( 1 ((ay 1)(by 1))) (-1 ((by 2))))
				  (0 < ( 1 ((bx 1)(cx 1))) (-1 ((bx 1)(ax 1))) (-1 ((ax 1)(cx 1))) ( 1 ((ax 2)))
				     ( 1 ((by 1)(cy 1))) (-1 ((ay 1)(by 1))) (-1 ((ay 1)(cy 1))) ( 1 ((ay 2))))
                                  (0 = (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1)))))
			    (4_a  ((1 ((ax 1))) = (1 ((cx 1))))
				((1 ((ay 1))) = (1 ((cy 1))))
				(0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a /= b
				   (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))
			    (b_4  ((1 ((bx 1))) = (1 ((cx 1))))
				  ((1 ((by 1))) = (1 ((cy 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a /= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))
			    (?_5  (0 > (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1))) ; applies to 1_5, 2_5, 3_5 (left hand side)
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a /= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))
			    (1_5 (0 < (1 ((bx 1) (cx 1))) (-1 ((bx 2))) (-1 ((ax 1) (cx 1))) (1 ((ax 1) (bx 1))) (1 ((by 1) (cy 1)))
				    (-1 ((by 2))) (-1 ((ay 1) (cy 1))) (1 ((ay 1) (by 1)))))
			    (2_5 (0 = (1 ((ax 1) (cx 1))) (-1 ((bx 1) (ax 1))) (-1 ((bx 1) (cx 1))) (1 ((bx 2))) (1 ((ay 1) (cy 1)))
				    (-1 ((by 1) (ay 1))) (-1 ((by 1) (cy 1))) (1 ((by 2)))))
			    (3_5 (0 < (1 ((bx 1) (cx 1))) (-1 ((ax 1) (bx 1))) (-1 ((ax 1) (cx 1))) (1 ((ax 2))) (1 ((by 1) (cy 1)))
				    (-1 ((ay 1) (by 1))) (-1 ((ay 1) (cy 1))) (1 ((ay 2))))
				 (0 < (1 ((ax 1) (cx 1))) (-1 ((bx 1) (ax 1))) (-1 ((bx 1) (cx 1))) (1 ((bx 2))) (1 ((ay 1) (cy 1)))
				    (-1 ((by 1) (ay 1))) (-1 ((by 1) (cy 1))) (1 ((by 2)))))
			    (3_6  (0 = (1 ((bx 1) (cx 1))) (-1 ((ax 1) (bx 1))) (-1 ((ax 1) (cx 1))) (1 ((ax 2))) (1 ((by 1) (cy 1)))
				     (-1 ((ay 1) (by 1))) (-1 ((ay 1) (cy 1))) (1 ((ay 2))))
				  (0 > (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a /= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))
			    (3_7  (0 < (1 ((ax 1) (cx 1))) (-1 ((ax 2))) (-1 ((bx 1) (cx 1))) (1 ((bx 1) (ax 1))) (1 ((ay 1) (cy 1))) 
				     (-1 ((ay 2))) (-1 ((by 1) (cy 1))) (1 ((by 1) (ay 1))))
				  (0 > (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a /= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))

			    (?_3  (0 < (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1))) ; applies to 7_3, 6_3, 5_3 (right hand side)
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a/= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))
			    (7_3 (0 < (1 ((bx 1) (cx 1))) (-1 ((bx 2))) (-1 ((ax 1) (cx 1))) (1 ((ax 1) (bx 1))) (1 ((by 1) (cy 1)))
				    (-1 ((by 2))) (-1 ((ay 1) (cy 1))) (1 ((ay 1) (by 1)))))
			    (6_3 (0 = (1 ((ax 1) (cx 1))) (-1 ((bx 1) (ax 1))) (-1 ((bx 1) (cx 1))) (1 ((bx 2))) (1 ((ay 1) (cy 1)))
				    (-1 ((by 1) (ay 1))) (-1 ((by 1) (cy 1))) (1 ((by 2)))))
			    (5_3 (0 < (1 ((bx 1) (cx 1))) (-1 ((ax 1) (bx 1))) (-1 ((ax 1) (cx 1))) (1 ((ax 2))) (1 ((by 1) (cy 1)))
				    (-1 ((ay 1) (by 1))) (-1 ((ay 1) (cy 1))) (1 ((ay 2))))
				 (0 < (1 ((ax 1) (cx 1))) (-1 ((bx 1) (ax 1))) (-1 ((bx 1) (cx 1))) (1 ((bx 2))) (1 ((ay 1) (cy 1)))
				    (-1 ((by 1) (ay 1))) (-1 ((by 1) (cy 1))) (1 ((by 2)))))
			    (5_2  (0 = (1 ((bx 1) (cx 1))) (-1 ((ax 1) (bx 1))) (-1 ((ax 1) (cx 1))) (1 ((ax 2))) (1 ((by 1) (cy 1)))
				     (-1 ((ay 1) (by 1))) (-1 ((ay 1) (cy 1))) (1 ((ay 2))))
				  (0 < (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a/= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2)))))
			    (5_1  (0 < (1 ((ax 1) (cx 1))) (-1 ((ax 2))) (-1 ((bx 1) (cx 1))) (1 ((bx 1) (ax 1))) (1 ((ay 1) (cy 1))) 
				     (-1 ((ay 2))) (-1 ((by 1) (cy 1))) (1 ((by 1) (ay 1))))
				  (0 < (-1 ((ax 1)(by 1))) ( 1 ((ax 1)(cy 1))) ( 1 ((ay 1)(bx 1)))
				     (-1 ((ay 1)(cx 1))) (-1 ((bx 1)(cy 1))) ( 1 ((by 1)(cx 1))))
				  (0 < (1 ((ax 2))) (-2 ((ax 1) (bx 1))) (1 ((bx 2))) ; a/= b
				     (1 ((ay 2))) (-2 ((ay 1) (by 1))) (1 ((by 2))))))
  :composition-operation (( 0_4 0_4 (0_4))
			  ( 0_4 1_5 (1_5))
			  ( 0_4 2_5 (1_5))
			  ( 0_4 3_5 (1_5))
			  ( 0_4 3_6 (2_5))
			  ( 0_4 3_7 (3_5 3_6 3_7))
			  ( 0_4 4_0 (4_0 4_4 4_A))
			  ( 0_4 5_1 (5_1 5_2 5_3))
			  ( 0_4 5_2 (6_3))
			  ( 0_4 5_3 (7_3))
			  ( 0_4 6_3 (7_3))
			  ( 0_4 7_3 (7_3))
			  ( 0_4 4_4 (0_4))
			  ( 0_4 4_a (B_4))
			  ( 0_4 b_4 (0_4))
			  ( 0_4 dou NIL)
			  ( 0_4 tri NIL)
			  ( 1_5 0_4 (1_5))
			  ( 1_5 1_5 (1_5 2_5 3_5 3_6 3_7))
			  ( 1_5 2_5 (1_5 2_5 3_5 3_6 3_7))
			  ( 1_5 3_5 (1_5 2_5 3_5 3_6 3_7))
			  ( 1_5 3_6 (3_5 3_6 3_7))
			  ( 1_5 3_7 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 1_5 4_0 (5_1 5_2 5_3))
			  ( 1_5 5_1 (5_1 5_2 5_3 6_3 7_3))
			  ( 1_5 5_2 (7_3))
			  ( 1_5 5_3 (0_4 1_5 7_3))
			  ( 1_5 6_3 (0_4 1_5 7_3))
			  ( 1_5 7_3 (0_4 1_5 7_3))
			  ( 1_5 4_4 (1_5))
			  ( 1_5 4_a (B_4))
			  ( 1_5 b_4 (1_5))
			  ( 1_5 dou NIL)
			  ( 1_5 tri NIL)
			  ( 2_5 0_4 (2_5))
			  ( 2_5 1_5 (3_5 3_6 3_7))
			  ( 2_5 2_5 (3_5 3_6 3_7))
			  ( 2_5 3_5 (3_5 3_6 3_7))
			  ( 2_5 3_6 (4_0 4_4 4_A))
			  ( 2_5 3_7 (5_1 5_2 5_3))
			  ( 2_5 4_0 (6_3))
			  ( 2_5 5_1 (7_3))
			  ( 2_5 5_2 (0_4))
			  ( 2_5 5_3 (1_5))
			  ( 2_5 6_3 (1_5))
			  ( 2_5 7_3 (1_5))
			  ( 2_5 4_4 (2_5))
			  ( 2_5 4_a (B_4))
			  ( 2_5 b_4 (2_5))
			  ( 2_5 dou NIL)
			  ( 2_5 tri NIL)
			  ( 3_5 0_4 (3_5 3_6 3_7))
			  ( 3_5 1_5 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 3_5 2_5 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 3_5 3_5 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 3_5 3_6 (5_1 5_2 5_3))
			  ( 3_5 3_7 (5_1 5_2 5_3 6_3 7_3))
			  ( 3_5 4_0 (7_3))
			  ( 3_5 5_1 (0_4 1_5 7_3))
			  ( 3_5 5_2 (1_5))
			  ( 3_5 5_3 (1_5 2_5 3_5 ))
			  ( 3_5 6_3 (1_5 2_5 3_5 ))
			  ( 3_5 7_3 (1_5 2_5 3_5 3_6 3_7))
			  ( 3_5 4_4 (3_5))
			  ( 3_5 4_a (B_4))
			  ( 3_5 b_4 (3_5))
			  ( 3_5 dou NIL)
			  ( 3_5 tri NIL)
			  ( 3_6 0_4 (3_7))
			  ( 3_6 1_5 (3_7 4_0 5_1))
			  ( 3_6 2_5 (3_7 4_0 5_1))
			  ( 3_6 3_5 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 3_6 3_6 (5_1 5_2 5_3))
			  ( 3_6 3_7 (5_1 5_2 5_3 6_3 7_3))
			  ( 3_6 4_0 (7_3))
			  ( 3_6 5_1 (0_4 1_5 7_3))
			  ( 3_6 5_2 (1_5))
			  ( 3_6 5_3 (1_5 2_5 3_5))
			  ( 3_6 6_3 (1_5 2_5 3_5))
			  ( 3_6 7_3 (1_5 2_5 3_5 3_6 3_7))
			  ( 3_6 4_4 (3_5))
			  ( 3_6 4_a (B_4))
			  ( 3_6 b_4 (3_6))
			  ( 3_6 dou NIL)
			  ( 3_6 tri NIL)
			  ( 3_7 0_4 (3_7))
			  ( 3_7 1_5 (3_7 4_0 5_1 ))
			  ( 3_7 2_5 (3_7 4_0 5_1 ))
			  ( 3_7 3_5 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 3_7 3_6 (5_1 5_2 5_3))
			  ( 3_7 3_7 (5_1 5_2 5_3 6_3 7_3))
			  ( 3_7 4_0 (7_3))
			  ( 3_7 5_1 (0_4 1_5 7_3))
			  ( 3_7 5_2 (1_5))
			  ( 3_7 5_3 (1_5 2_5 3_5 3_6 3_7))
			  ( 3_7 6_3 (1_5 2_5 3_5 3_6 3_7))
			  ( 3_7 7_3 (1_5 2_5 3_5 3_6 3_7))
			  ( 3_7 4_4 (3_5 3_6 3_7))
			  ( 3_7 4_a (B_4))
			  ( 3_7 b_4 (3_7))
			  ( 3_7 dou NIL)
			  ( 3_7 tri NIL)
			  ( 4_0 0_4 (4_0))
			  ( 4_0 1_5 (5_1))
			  ( 4_0 2_5 (5_1))
			  ( 4_0 3_5 (5_1 5_2 5_3))
			  ( 4_0 3_6 (6_3))
			  ( 4_0 3_7 (7_3))
			  ( 4_0 4_0 (0_4))
			  ( 4_0 5_1 (1_5))
			  ( 4_0 5_2 (2_5))
			  ( 4_0 5_3 (3_5 3_6 3_7))
			  ( 4_0 6_3 (3_7))
			  ( 4_0 7_3 (3_7))
			  ( 4_0 4_4 (4_0 4_4 4_A))
			  ( 4_0 4_a (B_4))
			  ( 4_0 b_4 (4_0))
			  ( 4_0 dou NIL)
			  ( 4_0 tri NIL)
			  ( 5_1 0_4 (5_1))
			  ( 5_1 1_5 (5_1 5_2 5_3 6_3 7_3))
			  ( 5_1 2_5 (5_1 5_2 5_3 6_3 7_3))
			  ( 5_1 3_5 (5_1 5_2 5_3 6_3 7_3))
			  ( 5_1 3_6 (7_3))
			  ( 5_1 3_7 (0_4 1_5 7_3))
			  ( 5_1 4_0 (1_5))
			  ( 5_1 5_1 (1_5 2_5 3_5 3_6 3_7))
			  ( 5_1 5_2 (3_5 3_6 3_7))
			  ( 5_1 5_3 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 5_1 6_3 (3_7 4_0 5_1))
			  ( 5_1 7_3 (3_7 4_0 5_1))
			  ( 5_1 4_4 (5_1 5_2 5_3))
			  ( 5_1 4_a (B_4))
			  ( 5_1 b_4 (5_1))
			  ( 5_1 dou NIL)
			  ( 5_1 tri NIL)
			  ( 5_2 0_4 (5_1))
			  ( 5_2 1_5 (5_1 5_2 5_3 6_3 7_3))
			  ( 5_2 2_5 (5_3 6_3 7_3))
			  ( 5_2 3_5 (5_3 6_3 7_3))
			  ( 5_2 3_6 (7_3))
			  ( 5_2 3_7 (0_4 1_5 7_3))
			  ( 5_2 4_0 (1_5))
			  ( 5_2 5_1 (1_5 2_5 3_5 3_6 3_7))
			  ( 5_2 5_2 (3_5 3_6 3_7))
			  ( 5_2 5_3 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 5_2 6_3 (3_7 4_0 5_1))
			  ( 5_2 7_3 (3_7 4_0 5_1))
			  ( 5_2 4_4 (5_3))
			  ( 5_2 4_a (B_4))
			  ( 5_2 b_4 (5_2))
			  ( 5_2 dou NIL)
			  ( 5_2 tri NIL)
			  ( 5_3 0_4 (5_1 5_2 5_3))
			  ( 5_3 1_5 (5_1 5_2 5_3 6_3 7_3))
			  ( 5_3 2_5 (5_3 6_3 7_3))
			  ( 5_3 3_5 (5_3 6_3 7_3))
			  ( 5_3 3_6 (7_3))
			  ( 5_3 3_7 (0_4 1_5 7_3))
			  ( 5_3 4_0 (1_5))
			  ( 5_3 5_1 (1_5 2_5 3_5 3_6 3_7))
			  ( 5_3 5_2 (3_5 3_6 3_7))
			  ( 5_3 5_3 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 5_3 6_3 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 5_3 7_3 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 5_3 4_4 (5_3))
			  ( 5_3 4_a (B_4))
			  ( 5_3 b_4 (5_3))
			  ( 5_3 dou NIL)
			  ( 5_3 tri NIL)
			  ( 6_3 0_4 (6_3))
			  ( 6_3 1_5 (7_3))
			  ( 6_3 2_5 (7_3))
			  ( 6_3 3_5 (7_3))
			  ( 6_3 3_6 (0_4))
			  ( 6_3 3_7 (1_5))
			  ( 6_3 4_0 (2_5))
			  ( 6_3 5_1 (3_5 3_6 3_7))
			  ( 6_3 5_2 (4_0 4_4 4_A))
			  ( 6_3 5_3 (5_1 5_2 5_3))
			  ( 6_3 6_3 (5_1 5_2 5_3))
			  ( 6_3 7_3 (5_1 5_2 5_3))
			  ( 6_3 4_4 (6_3))
			  ( 6_3 4_a (B_4))
			  ( 6_3 b_4 (6_3))
			  ( 6_3 dou NIL)
			  ( 6_3 tri NIL)
			  ( 7_3 0_4 (7_3))
			  ( 7_3 1_5 (0_4 1_5 7_3))
			  ( 7_3 2_5 (0_4 1_5 7_3))
			  ( 7_3 3_5 (0_4 1_5 7_3))
			  ( 7_3 3_6 (1_5))
			  ( 7_3 3_7 (1_5 2_5 3_5 3_6 3_7))
			  ( 7_3 4_0 (3_5 3_6 3_7))
			  ( 7_3 5_1 (3_5 3_6 3_7 4_0 5_1 5_2 5_3 4_4 4_A))
			  ( 7_3 5_2 (5_1 5_2 5_3))
			  ( 7_3 5_3 (5_1 5_2 5_3 6_3 7_3))
			  ( 7_3 6_3 (5_1 5_2 5_3 6_3 7_3))
			  ( 7_3 7_3 (5_1 5_2 5_3 6_3 7_3))
			  ( 7_3 4_4 (7_3))
			  ( 7_3 4_a (B_4))
			  ( 7_3 b_4 (7_3))
			  ( 7_3 dou NIL)
			  ( 7_3 tri NIL)
			  ( 4_4 0_4 (4_0 4_4 4_A))
			  ( 4_4 1_5 (5_1 5_2 5_3))
			  ( 4_4 2_5 (5_3))
			  ( 4_4 3_5 (5_3))
			  ( 4_4 3_6 (6_3))
			  ( 4_4 3_7 (7_3))
			  ( 4_4 4_0 (0_4))
			  ( 4_4 5_1 (1_5))
			  ( 4_4 5_2 (2_5))
			  ( 4_4 5_3 (3_5))
			  ( 4_4 6_3 (3_5))
			  ( 4_4 7_3 (3_5 3_6 3_7))
			  ( 4_4 4_4 (4_4))
			  ( 4_4 4_a (B_4))
			  ( 4_4 b_4 (4_4))
			  ( 4_4 dou NIL)
			  ( 4_4 tri NIL)
			  ( 4_a 0_4 (4_0))
			  ( 4_a 1_5 (5_1))
			  ( 4_a 2_5 (5_2))
			  ( 4_a 3_5 (5_3))
			  ( 4_a 3_6 (6_3))
			  ( 4_a 3_7 (7_3))
			  ( 4_a 4_0 (0_4))
			  ( 4_a 5_1 (1_5))
			  ( 4_a 5_2 (2_5))
			  ( 4_a 5_3 (3_5))
			  ( 4_a 6_3 (3_6))
			  ( 4_a 7_3 (3_7))
			  ( 4_a 4_4 (4_4))
			  ( 4_a 4_a (B_4))
			  ( 4_a b_4 (4_A))
			  ( 4_a dou NIL)
			  ( 4_a tri NIL)
			  ( b_4 0_4 NIL)
			  ( b_4 1_5 NIL)
			  ( b_4 2_5 NIL)
			  ( b_4 3_5 NIL)
			  ( b_4 3_6 NIL)
			  ( b_4 3_7 NIL)
			  ( b_4 4_0 NIL)
			  ( b_4 5_1 NIL)
			  ( b_4 5_2 NIL)
			  ( b_4 5_3 NIL)
			  ( b_4 6_3 NIL)
			  ( b_4 7_3 NIL)
			  ( b_4 4_4 NIL)
			  ( b_4 4_a NIL)
			  ( b_4 b_4 NIL)
			  ( b_4 dou (0_4 1_5 2_5 3_5 3_6 3_7 4_0 5_1 5_2 5_3 6_3 7_3 4_4 4_A))
			  ( b_4 tri (B_4))
			  ( dou 0_4 (DOU))
			  ( dou 1_5 (DOU))
			  ( dou 2_5 (DOU))
			  ( dou 3_5 (DOU))
			  ( dou 3_6 (DOU))
			  ( dou 3_7 (DOU))
			  ( dou 4_0 (DOU))
			  ( dou 5_1 (DOU))
			  ( dou 5_2 (DOU))
			  ( dou 5_3 (DOU))
			  ( dou 6_3 (DOU))
			  ( dou 7_3 (DOU))
			  ( dou 4_4 (DOU))
			  ( dou 4_a (TRI))
			  ( dou b_4 (DOU))
			  ( dou dou NIL)
			  ( dou tri NIL)
			  ( tri 0_4 NIL)
			  ( tri 1_5 NIL)
			  ( tri 2_5 NIL)
			  ( tri 3_5 NIL)
			  ( tri 3_6 NIL)
			  ( tri 3_7 NIL)
			  ( tri 4_0 NIL)
			  ( tri 5_1 NIL)
			  ( tri 5_2 NIL)
			  ( tri 5_3 NIL)
			  ( tri 6_3 NIL)
			  ( tri 7_3 NIL)
			  ( tri 4_4 NIL)
			  ( tri 4_a NIL)
			  ( tri b_4 NIL)
			  ( tri dou (DOU))
			  ( tri tri (TRI))))
