loa

Virtual machine for the Logic of Assumptions
git clone git://juanmeleiro.mat.br/loa
Log | Files | Refs

simple-case.lisp (687B)

      1 (assums (a x) (var x))
      2 (assums (b x) (var x))
      3 (assums (c x) (var x))
      4 
      5 ;; CTX := (NAME [ASSUM])
      6 ;; ASSUM := (NAME CTX EXPR [PROOF])
      7 ;; PROOF := (NAME => (NAME [PROOF]))
      8 
      9 (careful
     10 
     11  (a2b (vx () (var x) ()
     12        aa () (a x) (vx))
     13       (b x))
     14 
     15  (b2c (vx () (var x) ()
     16        ab () (b x) (vx))
     17       (c x)))
     18 
     19 (hasty
     20 
     21  (a2c (aa () (a x))
     22       (c x)))
     23 
     24 (implement hasty careful
     25 	   (a2c b2c
     26 		(ab a2b
     27 		    (a2c.aa))))
     28 
     29 (prove hasty.a2c ; goals: [a2c]
     30        careful.b2c ; goals: [careful.b2c.vx, careful.b2c.ab]
     31        triv ; goals: [careful.b2c.ab]
     32        careful.a2b ; goals: [careful.a2b.vx, careful.a2b.aa]
     33        triv ; goals: [careful.a2b.aa]
     34        hasty.a2c.aa ; goals: []
     35        )