Proof of proveit.numbers.ordering.max_x_x_is_x theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import x, y, defaults
from proveit.numbers.ordering import max_def_bin
In [2]:
%proving max_x_x_is_x
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
max_x_x_is_x:
(see dependencies)
max_x_x_is_x:
(see dependencies)
In [3]:
defaults.assumptions = max_x_x_is_x.conditions
defaults.assumptions: 
In [4]:
max_def_bin
In [5]:
max_def_bin_inst = max_def_bin.instantiate({x: x, y: x})
max_def_bin_inst: 
⊢ 
⊢ 
The rhs of the max_def_bin_inst above cannot be simplified until we explicitly establish that the second condition is False.
In [6]:
from proveit.numbers.ordering import not_less_from_less_eq
not_less_from_less_eq
In [7]:
not_less_from_less_eq.instantiate({x: x, y: x})
Now we can simplify the Max(x, x) definition in max_def_bin_inst:
In [8]:
max_def_bin_inst.inner_expr().rhs.simplify()
In [9]:
%qed
Out[9]:
