(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