Proof (kind2dev@731decdf5fb1.Proof)

val set_proof_logic : TermLib.logic -> unit

Set the logic used by the proof generations mechanism

val safety_proofname_cpc : string

Filename of the final proof of safety

val construct_kind_2_proof : 
  string ->
  string ->
  string ->
  string ->
  int ->
  unit

Creates the kind 2 CPC proofs of base, induction , and implication. Also outputs the combined "Safety CPC" proof of Kind 2

val construct_frontend_proof : 
  string ->
  string ->
  string ->
  string ->
  int ->
  unit

Creates the frontend (JKind) CPC proofs of base, induction , and implication. Also outputs the combined "Safety CPC" proof of the frontend

val construct_safety_proof : string -> unit

Combines the kind 2 and frontend safety CPC proofs into one proof of Safety in Safety CPC