(lambda (F n) (let (
  ; (ex (lambda (m e)(write (list m e))(newline) e))
  (G (apply (fileVal "gIntersect") (cdr F)))(n (+ n 1)))
(let ((rref (G 'rref))(id #f)(DoL ((fileVal "Do") 'DoL))(sg (car F)))
(lambda (sy) (let ((ans (assq sy (list
  (cons 'meet (G 'inter))
  (cons 'join (lambda (x y) (rref (append x y))))
  (cons 'zero '())
  (cons 're (lambda (k) (rref (DoL k (lambda (j) (DoL n (lambda (j) (sg))))))))
  (cons 'e= (let* (
     (fsub (cadr (cddddr F)))
     (fze? (caddr F))
     (gre (lambda (eq) (lambda (a b)
         (let e ((a a)(b b)) (or (and (null? a)(null? b))
            (and (eq (car a)(car b))(e (cdr a)(cdr b)))))))))
         (gre (gre (lambda (a b) (fze? (fsub a b)))))))))))
 (if ans (cdr ans) (and (eq? sy 'one) (or id
      (begin (set! id ((G 'iden) n)) id)))))))))

; test
(define P ((fileVal "PGc") (list ((fileVal "rr") "fit") 0 zero? 1 + - * /) 4))
(define p= (P 'e=))
(p= '() '())
(p= '((3 5)(3 6 7)) '((3 5)(3 6 7)))
(p= '((3 5)(3 6 7)) '((3 5)(3 5 7)))
(define pp (P 're))
(pp 2) ; => ((1 0 63763260/10609812403 -2544466980/24299892923 -208760970/1466064593) (0 1 -26071116/342252013 187828410808/24299892923 -1739632628/4398193779))
(define me (P 'meet))
(define jo (P 'join))
(define (tx i j k) (lambda (up dn) (let ((a (pp 1))(b (pp j))(c (pp k))) (and
   (p= (up a b)(up b a))
   (p= (up (up a b) c)(up a (up b c)))
   (p= (up a (dn a b)) a)
   (p= (up a a) a)))))
(define tl (tx 2 3 1))
(tl me jo) ; => #t
(tl jo me) ; => #t
(let r ((n 100)) (or (= n 0) (and (tl me jo) (tl jo me) (r (- n 1)))))
