kdrag.kernel.lemma

kdrag.kernel.lemma(thm: BoolRef, by: list[None] = [], admit=False, timeout=1000, dump=False, solver=None) → None

Prove a theorem using a list of previously proved lemmas.

In essence prove(Implies(by, thm)).

Parameters:

  • thm (smt.BoolRef) – The theorem to prove.

  • thm – The theorem to prove.

  • by (list[Proof]) – A list of previously proved lemmas.

  • admit (bool) – If True, admit the theorem without proof.

Returns:

A proof object of thm

Return type:

Proof

>>> lemma(BoolVal(True))

>>> lemma(RealVal(1) >= RealVal(0))