Theorems (or conjectures) for the theory of proveit.logic.booleans.quantification.universality

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Function
from proveit.logic import Equals, Implies, And, Forall, in_bool
from proveit.numbers import Add, num
from proveit import n, m, P, Q, R
from proveit.core_expr_types import (
    x_1_to_n, x_1_to_np1, y_1_to_m, P__x_1_to_n, P__x_1_to_np1    
)
from proveit.logic.booleans.quantification import (
    general_forall_Px_if_Qx, general_nested_forall_Pxy_if_Qx, 
    general_bundled_forall_Pxy_if_Qx)
from proveit.numbers import Natural, NaturalPos
%begin theorems

Defining theorems for theory 'proveit.logic.booleans.quantification.universality'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

forall_with_conditions__is_bool = Forall(n, Forall((P, Q), in_bool(general_forall_Px_if_Qx)),
                                         domain=NaturalPos)

forall_with_conditions__is_bool (conjecture with conjecture-based proof):

bundling = \
    Forall((m, n), Forall((P, Q, R), 
                          Equals(general_nested_forall_Pxy_if_Qx,
                                 general_bundled_forall_Pxy_if_Qx) \
                          .with_wrapping_at(1)),
           domain=NaturalPos)

bundling (conjecture without proof):

bundle = Forall((m, n), Forall((P, Q, R), 
                               Implies(general_nested_forall_Pxy_if_Qx,
                                       general_bundled_forall_Pxy_if_Qx) \
                               .with_wrapping_at(1)),
                  domain=NaturalPos)

bundle (conjecture without proof):

unbundle = Forall((m, n), Forall((P, Q, R), 
                                 Implies(general_bundled_forall_Pxy_if_Qx,
                                         general_nested_forall_Pxy_if_Qx) \
                                 .with_wrapping_at(1)),
                    domain=NaturalPos)

unbundle (conjecture without proof):

Induction to any number of $\forall$ instance variables:

forall_induction = \
    Forall(P, Implies(And(Function(P, []),
                          Forall(n, Implies(Forall(x_1_to_n, P__x_1_to_n),
                                            Forall(x_1_to_np1, P__x_1_to_np1)) \
                                    .with_wrap_after_operator(),
                                 domain=Natural)),
                      Forall(n, Forall(x_1_to_n, P__x_1_to_n),
                             domain=Natural)).with_wrap_before_operator())

forall_induction (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.logic.booleans.quantification.universality