Common expressions for the theory of proveit.logic

import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import Function
from proveit import fx, gx, P, Q
from proveit.logic import TRUE, FALSE, Implies, Equals
%begin common

Defining common sub-expressions for theory 'proveit.logic'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions

fx_eq_gx = Equals(fx, gx)

fx_eq_gx:

PofTrue = Function(P, TRUE)

PofTrue:

PofFalse = Function(P, FALSE)

PofFalse:

QimplPofTrue = Implies(Function(Q, TRUE), PofTrue)

QimplPofTrue:

QimplPofFalse = Implies(Function(Q, FALSE), PofFalse)

QimplPofFalse:

%end common

These common expressions may now be imported from the theory package: proveit.logic