logo

Common expressions for the theory of proveit.logic.booleans.quantification

In [1]:
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 k, A, B
from proveit.core_expr_types import (
    x_1_to_n, x_1_to_m, y_1_to_n, y_1_to_m, z_1_to_n, 
    P__x_1_to_n, P__y_1_to_n, P__x_1_to_m_y_1_to_n, 
    Q__x_1_to_n, Q__x_1_to_m, Q__y_1_to_n, Q__z_1_to_n, R__x_1_to_n, 
    R__y_1_to_m, R__z_1_to_n, R__x_1_to_m_y_1_to_n)
from proveit.logic import TRUE, Implies, Not, Forall, Exists, NotExists, NotEquals
from proveit.numbers import Natural, NaturalPos
%begin common
Defining common sub-expressions for theory 'proveit.logic.booleans.quantification'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [2]:
general_forall_Px = Forall(x_1_to_n, P__x_1_to_n)
general_forall_Px:
In [3]:
general_forall_Py= Forall(y_1_to_n, P__y_1_to_n)
general_forall_Py:
In [4]:
general_forall_Px_if_Qx = Forall(x_1_to_n, P__x_1_to_n, conditions=[Q__x_1_to_n])
general_forall_Px_if_Qx:
In [5]:
general_forall_Py_if_Qy = Forall(y_1_to_n, P__y_1_to_n, conditions=[Q__y_1_to_n])
general_forall_Py_if_Qy:
In [6]:
general_nested_forall_Pxy_if_Qx = Forall(x_1_to_m, 
                                         Forall(y_1_to_n, P__x_1_to_m_y_1_to_n,
                                                conditions=R__x_1_to_m_y_1_to_n),
                                         conditions=Q__x_1_to_m)
general_nested_forall_Pxy_if_Qx:
In [7]:
general_bundled_forall_Pxy_if_Qx = Forall((x_1_to_m, y_1_to_n), 
                                          P__x_1_to_m_y_1_to_n,
                                          conditions=[Q__x_1_to_m, R__x_1_to_m_y_1_to_n])
general_bundled_forall_Pxy_if_Qx:
In [8]:
general_forall__Py_not_T = Forall(y_1_to_n, NotEquals(P__y_1_to_n, TRUE))
general_forall__Py_not_T:
In [9]:
general_forall__Py_not_T__st_Qy = Forall(y_1_to_n, NotEquals(P__y_1_to_n, TRUE),
                                        conditions = [Q__y_1_to_n])
general_forall__Py_not_T__st_Qy:
In [10]:
general_forall_st_Qx__Px_implies_Rx = Forall(x_1_to_n, Implies(P__x_1_to_n, R__x_1_to_n),
                                             conditions=[Q__x_1_to_n])
general_forall_st_Qx__Px_implies_Rx:
In [11]:
general_exists_Px = Exists(x_1_to_n, P__x_1_to_n)
general_exists_Px:
In [12]:
general_exists_Px_st_Qx = Exists(x_1_to_n, P__x_1_to_n,
                                 conditions=[Q__x_1_to_n])
general_exists_Px_st_Qx:
In [13]:
general_exists_in_A_Px_st_Qx = Exists(x_1_to_n, P__x_1_to_n, domain=A,
                                      conditions=[Q__x_1_to_n])
general_exists_in_A_Px_st_Qx:
In [14]:
general_exists_Py = Exists(y_1_to_n, P__y_1_to_n)
general_exists_Py:
In [15]:
general_exists_Py_st_Qy = Exists(y_1_to_n, P__y_1_to_n, conditions=[Q__y_1_to_n])
general_exists_Py_st_Qy:
In [16]:
general_exists_Rz_st_Qz = Exists(z_1_to_n, R__z_1_to_n, conditions=[Q__z_1_to_n])
general_exists_Rz_st_Qz:
In [17]:
general_exists_in_B_Py_st_Qy = Exists(y_1_to_n, P__y_1_to_n, domain=B,
                                      conditions=[Q__y_1_to_n])
general_exists_in_B_Py_st_Qy:
In [18]:
general_exists_notPx = Exists(x_1_to_n, Not(P__x_1_to_n))
general_exists_notPx:
In [19]:
general_exists_notPx_st_Qx = Exists(x_1_to_n, Not(P__x_1_to_n),
                                    conditions=[Q__x_1_to_n])
general_exists_notPx_st_Qx:
In [20]:
general_notexists_Px = NotExists(x_1_to_n, P__x_1_to_n)
general_notexists_Px:
In [21]:
general_notexists_Px_st_Qx = NotExists(x_1_to_n, P__x_1_to_n, conditions=[Q__x_1_to_n])
general_notexists_Px_st_Qx:
In [22]:
general_notexists_Py = NotExists(y_1_to_n, P__y_1_to_n)
general_notexists_Py:
In [23]:
general_notexists_Py_st_Qy = NotExists(y_1_to_n, P__y_1_to_n,
                                       conditions=[Q__y_1_to_n])
general_notexists_Py_st_Qy:
In [24]:
general_notexists_notPy = NotExists(y_1_to_n, Not(P__y_1_to_n))
general_notexists_notPy:
In [25]:
general_notexists_notPy_st_Qy = NotExists(y_1_to_n, Not(P__y_1_to_n),
                                          conditions=[Q__y_1_to_n])
general_notexists_notPy_st_Qy:
In [26]:
%end common
These common expressions may now be imported from the theory package: proveit.logic.booleans.quantification