proveit is a command line utility for running the theorem prover in batch mode.

$ proveit --importchain --clean interval_arith/top.pvs

<code text nasalib_bag> use_bag : THEORY BEGIN

IMPORTING structures@bags
% NASA library

% All the conjectures prove with grind

test1: CONJECTURE
  member(5,insert(5,emptybag)) = 1

%|- test1 : PROOF %|- (grind) %|- QED

test2: CONJECTURE
      count(1, emptybag) = 0 
  AND count(1, insert(1, emptybag)) = 1
  AND count(1, insert(1, insert(1, emptybag))) = 2

%|- test2 : PROOF %|- (grind) %|- QED

PRODUCT: TYPE = posnat
prd, prd1, prd2: VAR PRODUCT

SET_PRODUCT: TYPE = setof[PRODUCT]
sp, sp1, sp2: VAR SET_PRODUCT

 % add product p to set of products sp
add_type(p:PRODUCT,sp): SET_PRODUCT = 
  union(singleton(p), sp)

%IMPORTING structures@bags[PRODUCT]
STOCK: TYPE = bag[PRODUCT]
st, st1, st2: VAR STOCK

add_product(st1, st): STOCK = % add st1 to stock st if dom(st1)
  plus(st1, st)

p1,p2,p3: PRODUCT

test3: CONJECTURE
  st = emptybag WITH [p1 := 1, p2 := 2] implies count(p2, st) = 2

%|- test3 : PROOF %|- (grind) %|- QED

cart1: bag[PRODUCT] = emptybag WITH [p1 := 1, p2 := 2]

%insert(x,b): bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF)
test4: CONJECTURE
  p3 /= p2 AND p2 /= p1 AND p1 /= p3 => count(p3, cart1) = 0

%|- test4 : PROOF %|- (grind) %|- QED

END use_bag <code>