Assumption

class proveit.Assumption(expr, assumptions=None, *, _proven_truth=None, _requirements=None, _marked_req_indices=None)

Bases: proveit.Proof

Attributes Summary

all_assumptions

Methods Summary

make_assumption(expr)	Return an Assumption object, only creating it if it doesn’t already exist.
step_type(self)

Attributes Documentation

all_assumptions = {_b = _a: step type requirements statement 0 assumption {_b = _a} |- _b = _a , x = y: step type requirements statement 0 assumption {x = y} |- x = y , _a = TRUE: step type requirements statement 0 assumption {_a = TRUE} |- _a = TRUE , A = TRUE: step type requirements statement 0 assumption {A = TRUE} |- A = TRUE , _a: step type requirements statement 0 assumption {_a} |- _a , A: step type requirements statement 0 assumption {A} |- A , _a in BOOLEAN: step type requirements statement 0 assumption {_a in BOOLEAN} |- _a in BOOLEAN , A in BOOLEAN: step type requirements statement 0 assumption {A in BOOLEAN} |- A in BOOLEAN , (_a = TRUE) or (_a = FALSE): step type requirements statement 0 assumption {(_a = TRUE) or (_a = FALSE)} |- (_a = TRUE) or (_a = FALSE) , (A = TRUE) or (A = FALSE): step type requirements statement 0 assumption {(A = TRUE) or (A = FALSE)} |- (A = TRUE) or (A = FALSE) , [not](_a) in BOOLEAN: step type requirements statement 0 assumption {[not](_a) in BOOLEAN} |- [not](_a) in BOOLEAN , [not](A) in BOOLEAN: step type requirements statement 0 assumption {[not](A) in BOOLEAN} |- [not](A) in BOOLEAN , _a = FALSE: step type requirements statement 0 assumption {_a = FALSE} |- _a = FALSE , A = FALSE: step type requirements statement 0 assumption {A = FALSE} |- A = FALSE , [not]([not](_a)): step type requirements statement 0 assumption {[not]([not](_a))} |- [not]([not](_a)) , [not]([not](A)): step type requirements statement 0 assumption {[not]([not](A))} |- [not]([not](A)) , FALSE: step type requirements statement 0 assumption {FALSE} |- FALSE , [not](_a) => FALSE: step type requirements statement 0 assumption {[not](_a) => FALSE} |- [not](_a) => FALSE , [not](A) => FALSE: step type requirements statement 0 assumption {[not](A) => FALSE} |- [not](A) => FALSE , _a => FALSE: step type requirements statement 0 assumption {_a => FALSE} |- _a => FALSE , A => FALSE: step type requirements statement 0 assumption {A => FALSE} |- A => FALSE , _b != _a: step type requirements statement 0 assumption {_b != _a} |- _b != _a , x != y: step type requirements statement 0 assumption {x != y} |- x != y , _a != FALSE: step type requirements statement 0 assumption {_a != FALSE} |- _a != FALSE , A != FALSE: step type requirements statement 0 assumption {A != FALSE} |- A != FALSE , [not](_b = _a): step type requirements statement 0 assumption {[not](_b = _a)} |- [not](_b = _a) , [not](x = y): step type requirements statement 0 assumption {[not](x = y)} |- [not](x = y) , _b proper_subset _a: step type requirements statement 0 assumption {_b proper_subset _a} |- _b proper_subset _a , A proper_subset B: step type requirements statement 0 assumption {A proper_subset B} |- A proper_subset B , _a in Natural: step type requirements statement 0 assumption {_a in Natural} |- _a in Natural , n in Natural: step type requirements statement 0 assumption {n in Natural} |- n in Natural , _b in Real: step type requirements statement 0 assumption {_b in Real} |- _b in Real , _a in Real: step type requirements statement 0 assumption {_a in Real} |- _a in Real , _b <= _a: step type requirements statement 0 assumption {_b <= _a} |- _b <= _a , x in Real: step type requirements statement 0 assumption {x in Real} |- x in Real , y in Real: step type requirements statement 0 assumption {y in Real} |- y in Real , x <= y: step type requirements statement 0 assumption {x <= y} |- x <= y , Natural: step type requirements statement 0 assumption {Natural} |- Natural , _c proper_subset _b: step type requirements statement 0 assumption {_c proper_subset _b} |- _c proper_subset _b , _a in _c: step type requirements statement 0 assumption {_a in _c} |- _a in _c , x in A: step type requirements statement 0 assumption {x in A} |- x in A , _a in RationalNonNeg: step type requirements statement 0 assumption {_a in RationalNonNeg} |- _a in RationalNonNeg , q in RationalNonNeg: step type requirements statement 0 assumption {q in RationalNonNeg} |- q in RationalNonNeg , _a in RealNonNeg: step type requirements statement 0 assumption {_a in RealNonNeg} |- _a in RealNonNeg , x in RealNonNeg: step type requirements statement 0 assumption {x in RealNonNeg} |- x in RealNonNeg , _a in IntegerNonPos: step type requirements statement 0 assumption {_a in IntegerNonPos} |- _a in IntegerNonPos , a in IntegerNonPos: step type requirements statement 0 assumption {a in IntegerNonPos} |- a in IntegerNonPos , _a in RationalNonPos: step type requirements statement 0 assumption {_a in RationalNonPos} |- _a in RationalNonPos , q in RationalNonPos: step type requirements statement 0 assumption {q in RationalNonPos} |- q in RationalNonPos , _a in RealNonPos: step type requirements statement 0 assumption {_a in RealNonPos} |- _a in RealNonPos , x in RealNonPos: step type requirements statement 0 assumption {x in RealNonPos} |- x in RealNonPos , _c subset_eq _b: step type requirements statement 0 assumption {_c subset_eq _b} |- _c subset_eq _b , A subset_eq B: step type requirements statement 0 assumption {A subset_eq B} |- A subset_eq B , [not](_b < _a): step type requirements statement 0 assumption {[not](_b < _a)} |- [not](_b < _a) , [not](x < y): step type requirements statement 0 assumption {[not](x < y)} |- [not](x < y) , _b < _a: step type requirements statement 0 assumption {_b < _a} |- _b < _a , x < y: step type requirements statement 0 assumption {x < y} |- x < y , a in Real: step type requirements statement 0 assumption {a in Real} |- a in Real , b in Real: step type requirements statement 0 assumption {b in Real} |- b in Real , a < b: step type requirements statement 0 assumption {a < b} |- a < b , [not](_b <= _a): step type requirements statement 0 assumption {[not](_b <= _a)} |- [not](_b <= _a) , [not](x <= y): step type requirements statement 0 assumption {[not](x <= y)} |- [not](x <= y) , _a in NaturalPos: step type requirements statement 0 assumption {_a in NaturalPos} |- _a in NaturalPos , n in NaturalPos: step type requirements statement 0 assumption {n in NaturalPos} |- n in NaturalPos , _a in IntegerNonZero: step type requirements statement 0 assumption {_a in IntegerNonZero} |- _a in IntegerNonZero , a in IntegerNonZero: step type requirements statement 0 assumption {a in IntegerNonZero} |- a in IntegerNonZero , _a in RationalNonZero: step type requirements statement 0 assumption {_a in RationalNonZero} |- _a in RationalNonZero , q in RationalNonZero: step type requirements statement 0 assumption {q in RationalNonZero} |- q in RationalNonZero , _a in RealNonZero: step type requirements statement 0 assumption {_a in RealNonZero} |- _a in RealNonZero , x in RealNonZero: step type requirements statement 0 assumption {x in RealNonZero} |- x in RealNonZero , _a in ComplexNonZero: step type requirements statement 0 assumption {_a in ComplexNonZero} |- _a in ComplexNonZero , x in ComplexNonZero: step type requirements statement 0 assumption {x in ComplexNonZero} |- x in ComplexNonZero , _a in RationalPos: step type requirements statement 0 assumption {_a in RationalPos} |- _a in RationalPos , q in RationalPos: step type requirements statement 0 assumption {q in RationalPos} |- q in RationalPos , _a in RealPos: step type requirements statement 0 assumption {_a in RealPos} |- _a in RealPos , x in RealPos: step type requirements statement 0 assumption {x in RealPos} |- x in RealPos }

Methods Documentation

static make_assumption(expr)

Return an Assumption object, only creating it if it doesn’t already exist. assumptions must already be ‘checked’ and in tuple form.

step_type(self)