(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* (
     (fadd (car (cddddr F)))
     (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? (fadd a (fsub 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= '() '()) ; => #t
(p= '((3 5)(3 6 7)) '((3 5)(3 6 7))) ; => #t
(p= '((3 5)(3 6 7)) '((3 5)(3 5 7))) ; => #f
(define pp (P 're))
(pp 2) ; => ((1 0 -9733695188/592309653 -15702259384/5692822299 1468534438/653880303) (0 1 1265769032/144075321 1559235152/2227626117 17530578269/58849227270))
(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))))) ; => #t
