Current Sequent  Applicable Proof Command[s] and Resulting Sequent[s] 
Universal consequent
...

(FORALL (a: A, b: B): alpha),
...  Applicable Proof Commands  Resulting Sequent[s]  Skolemization is straightforward. (skolem * ("aa" "bb"))
(skolem + ("aa" "bb")) 
...  alpha[a/aa; b/bb], ...  Partial skolemization (skolem * ("_" "bb"))
(skolem + ("_" "bb"))  ...

(FORALL (a: A): alpha[b/bb],
...  Well founded induction often requires human insight.
(induct "a")
(induct "b")  several sequents
corresponding to inductive cases 

Existential antecedent (EXISTS (a: A, b: B): alpha),
...  ...  Applicable Proof Commands  Resulting Sequent  Skolemization is straightforward.
(skolem * ("aa" "bb"))
(skolem  ("aa" "bb"))  alpha[a/aa; b/bb], ...  ... 

Universal consequent ...

(FORALL (a: (a?)): p(a)),
...  Applicable Proof Commands  Resulting Sequent  Explicit subtype information
(skolem * "aa" :skolemtypepreds? t)
(apply (then (skolem * "aa") (typepred "aa"))
see proof management below 
a?(aa), ...

p(aa), ... 

Specific consequent ...  p(eA), ...
assuming eA: A  Applicable Proof Commands  Resulting Sequent  Generalization is the inverse of skolemization: requires human insight and often precedes well founded induction.
(generalize "eA" "a") 
...  (FORALL (a: A): p(a)), ... 

Instantiation  often requires human insight: "eA" and "eB" templates may be complex expressions. 
Existential consequent ...  (EXISTS (a: A, b: B): alpha), ...  Applicable Proof Commands  Resulting Sequent

(inst * "eA" "eB")
(inst + "eA" "eB")
(inst?) 
...  alpha[a/eA; b/eB]
...  eA: A, ...
...  eB: B, ... 

Universal antecedent
(FORALL (a: A, b: B): alpha), ...

...  Applicable Proof Commands  Resulting Sequent 
(inst * "eA" "eB")
(inst  "eA" "eB")
(inst?)  alpha[a/eA; b/eB], ...  ...
...  eA: A, ...
...  eB: B, ... 
(instcp * "eA" "eB")
(instcp  "eA" "eB")  alpha[a/eA; b/eB], (FORALL (a: A, b: B): alpha), ...  ... ...  eA: A, ... ...  eB: B, ... same as above, except for preserving FORALL  
Flattening  usually simplifies sequent by removing some logical connectors 
 ...  alpha IMPLIES beta, ...  ...  alpha OR beta, ...  alpha AND beta, ...  ... 
 Applicable Proof Command  Resulting Sequent 
(flatten)  alpha, ...  beta, ...  ...  alpha, beta, ...  alpha, beta, ...  ... 


Case splitting  may complexify proof but is sometimes necessary 
 ...  alpha AND beta, ...  alpha OR beta, ...  ...  alpha IMPLIES beta, ...  ...  ..  alpha IFF beta, ...  ...  IF e THEN a ELSE b ENDIF, ...  ...  CASES e OF ... ENDCASES, ... 
 Applicable Proof Command  Resulting Sequents 
(split)  ...  alpha, ...
...  beta, ...  alpha, ...  ...
beta, ...  ...  ...  alpha, ...
beta, ...  ...  alpha, ...  beta, ...
beta, ...  alpha, ...  e, ...  a, ...
...  e, b, ...  several sequents 


...  ...  Applicable Proof Command  Resulting Sequents  Use a lemma on the fly. (case "alpha")  alpha, ...  ...
...  alpha, ... 

Toward  propositional calculus 
Boolean equality ...  ..., alpha = beta, ... provided alpha, beta: bool  Applicable Proof Command  Resulting Sequent  (iff)  ...  ..., alpha IFF beta 

Embedded test ...  p(IF e THEN a ELSE b ENDIF), ...  Embedded cases ...  p(CASES e OF ... ENDCASES), ... 
 Applicable Proof Command  Resulting Sequent 
(liftif) 
...  IF p(e) THEN p(a) ELSE p(b) ENDIF, ... 
...  CASES e OF ... ENDCASES, ... where p applies to each clause result 


Decision  procedures for propositional calculus and linear arithmetics 
propositional sequent NOT, AND, OR, IMPLIES, IFF IF, CASES  Applicable Proof Command  Resulting Sequents  (prop)  some sequents or none 

linear arithmetic sequent =, <=, >, >=  Applicable Proof Command  Resulting Sequents  (assert)  simplified sequent (or nomore sequent) 

propositional + linear arithmetic sequent
 Applicable Proof Command  Resulting Sequents 
(ground) 
some sequents or none 

Using  function definitions 
sequent containing f (...) typically with f non recursive  Applicable Proof Command  Resulting Sequent 
(expand "f") (expand "f" +) (expand "f" ) 
sequent with some f(...) function calls unfolded 

sequent containing f(...) typically with f recursive  Applicable Proof Command  Resulting Sequent 
(expand "f" :ifsimplifies t) 
f(...) calls are unfolded provided some simplification occurs 

... f(e_{1}) ... f(e_{2}) ...  ... f(e_{3}) ...  Applicable Proof Command  Resulting Sequent 
(expand "f" * 2) (expand "f"  2) 
... f(e_{1}) ... fe_{2}_unfolded ...  ... f(e_{3}) ... 

sequent containing f(...)  Applicable Proof Command  Resulting Sequent 
(autorewrite "f") 
sequent unchanged subsequent (ground) will automatically trigger (expand "f" :ifsimplifies t) 

Using  lemmas, theorems, corollaries or the like 
antecedents  consequents  Applicable Proof Command  Resulting Sequent[s] 
(lemma "foo") 
fooLemmaFormula, antecedents  consequents 
(use "foo") 
fooLemmaFormulaInstance, antecedents  consequents
combines (lemma "foo") and (inst?) 
(rewrite "foo") 
sequent with some term rewritten according to lemma main equality lemma hypotheses may trigger subgoals 
(rewrite "foo" :subst ("a" ... "b" ...)) 
same as above but specifies instantiation in part or whole 
(rewrite "foo" :dir RL) 
same as (rewrite "foo") except that main equality is applied from right to left 
(rewrite "foo" :fnums + :targetfnums +) 
same as (rewrite "foo") except that rewriting only occurs within consequents 
(autorewrite "foo") Useful if "foo" lemma is a good rewrite lemma 
sequent unchanged subseqent (ground) will trigger rewriting according to "foo" lemma if a match occurs and all lemma hypotheses can be proved 

Dealing with equality:  prefer (assert) whenever applicable 
proving function equality ...  f = g, ... assuming f, g: [T > U]  Applicable Proof Command  Resulting Sequent[s] 
(applyextensionality :hide? t) 
...  f(x!1) = g(x!1), ... 

Using an equality a = b, ...  ...  Applicable Proof Command  Resulting Sequent 
(replace 1 :hide? t) 
...[a/b]  ...[a/b] 
(replace 1 :hide? t :dir RL) 
...[b/a]  ...[b/a] 

Improve  readability 
hiding alpha_{1}, alpha_{2}, alpha_{3}  beta_{1} beta_{2}  Applicable Proof Command  Resulting Sequent 
(hide 2 3 1) may hinder proof robustness 
alpha_{1}  beta_{2} 

 beta_{1} 

renaming constants ..., p(X!1, X!2), ...  ..., q(X!2, Y!3), ...  Applicable Proof Command  Resulting Sequent 
(namereplace "b" "X!2")

.., p(X!1, b), ...  ..., q(b, Y!3), ... 
(namereplace* ("a" "X!1" "b" "X!2" "c" "X!3")) 
..., p(a, b), ...  ..., q(b, c), ... 

...  ...  Applicable Proof Command  Resulting Sequent 
(comment "Bla bla bla.") 
...  ... sequent is left unchanged 

...  ...  Applicable Proof Command  Resulting Sequent 
(apply (then c_{1} c_{2} c_{3})) 
sequent resulting from sequential application of commands c_{1}, c_{2}, c_{3} 
(undo) 
go back one proof step to parent sequent 
(postpone) 
switch to next sequent, therefore postponing current sequent proof 
(quit) quit 
quit PVS prover, saving current partial proof 

Recover from  PVS crash 
LISP error!!! (PVS bug)  Applicable Proof Command  Resulting Sequent 
(restore) 
goes back to previous coherent state of the proof, just before the proof command responsible for PVS crash 

Believe in  miracles! 
...  ...  Applicable Proof Command  Resulting Sequent[s]  (grind)  either some clumsy often unprovable sequents or finishes proof of sequent most powerful PVS proof command: OK to try, but undo if does not complete the proof 
