# Demonstrations for context proveit.logic.boolean.disjunction¶

In [1]:
import proveit
from proveit._common_ import A, B, C, D, E,F,G,H,I,J,K,L,AA, m
from proveit.number import num, Naturals
from proveit.logic import Booleans, inBool, InSet, Or, And, TRUE, FALSE, Not, Implies, Equals
from proveit.logic.boolean.disjunction._theorems_ import closure, eachInBool
%begin demonstrations

In [2]:
closure

Out[2]:
In [3]:
closure_spec = closure.specialize({m:m}, assumptions=[InSet(m, Naturals)])

Out[3]:
closure_spec:
In [4]:
closure.specialize({m:num(4)}, relabelMap={AA:C}, assumptions=[C])

Out[4]:
In [5]:
demo1 = closure.specialize({m:num(4), AA:[A, B, C, D]}, assumptions = [inBool(A), inBool(B), inBool(C), inBool(D)])

Out[5]:
demo1:
In [6]:
demo1.proof()

Out[6]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , :
1theorem
proveit.logic.boolean.disjunction.closure
2theorem
proveit.number.numeral.deci.nat4
3specialization7, 8, 9, 10, 11
: , : , : , : , :
4theorem
5theorem
6theorem
7theorem
proveit.logic.set_theory.membership.exp_set_4
8assumption
9assumption
10assumption
11assumption
In [7]:
demo1.element.deducePartInBool(1, assumptions=[demo1.expr, inBool(Or(A,B,C))])

Out[7]:
In [8]:
eachInBool

Out[8]:
In [ ]:


In [ ]:


In [9]:
Or(TRUE,TRUE).prove().proof()

Out[9]:
step typerequirementsstatement
0theorem
proveit.logic.boolean.disjunction.trueOrTrue
In [10]:
Or(TRUE,FALSE).prove().proof()

Out[10]:
step typerequirementsstatement
0theorem
proveit.logic.boolean.disjunction.trueOrFalse
In [11]:
Or(FALSE,TRUE).prove().proof()

Out[11]:
step typerequirementsstatement
0theorem
proveit.logic.boolean.disjunction.falseOrTrue
In [12]:
Not(Or(FALSE,FALSE)).prove().proof()

Out[12]:
step typerequirementsstatement
0theorem
proveit.logic.boolean.disjunction.falseOrFalseNegated
In [13]:
Or(A,B).prove([A,B]).proof()

Out[13]:
step typerequirementsstatement
0specialization1, 2, 3
: , :
1theorem
proveit.logic.boolean.disjunction.orIfBoth
2assumption
3assumption
In [14]:
Or(A,B).prove([A,Not(B)]).proof()

Out[14]:
step typerequirementsstatement
0specialization1, 2, 3
: , :
1theorem
proveit.logic.boolean.disjunction.orIfOnlyLeft
2assumption
3assumption
In [15]:
Or(A,B).prove([B,Not(A)]).proof()

Out[15]:
step typerequirementsstatement
0specialization1, 2, 3
: , :
1theorem
proveit.logic.boolean.disjunction.orIfOnlyRight
2assumption
3assumption
In [16]:
Not(Or(A,B)).prove([Not(A), Not(B)]).proof()

Out[16]:
step typerequirementsstatement
0specialization1, 2, 3
: , :
1theorem
proveit.logic.boolean.disjunction.neitherIntro
2assumption
3assumption
In [17]:
Or(A,B).deriveContradiction([Not(A),Not(B), Or(A,B)]).proof()

Out[17]:
step typerequirementsstatement
0specialization1, 2, 3, 4
: , :
1theorem
2assumption
3assumption
4assumption
In [18]:
Or(A,B).deriveLeftIfNotRight([inBool(A), inBool(B), Not(B), Or(A,B)]).proof()

Out[18]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5
: , :
1theorem
proveit.logic.boolean.disjunction.leftIfNotRight
2assumption
3assumption
4assumption
5assumption
In [19]:
Or(A,B).deriveRightIfNotLeft([*inBool(A,B), Not(A), Or(A,B)]).proof()

Out[19]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5
: , :
1theorem
proveit.logic.boolean.disjunction.rightIfNotLeft
2assumption
3assumption
4assumption
5assumption
In [20]:
Or(A,B).deriveViaDilemma(C,assumptions=[Or(A,B),inBool(B),Implies(A,C), Implies(B,C), inBool(A), Implies(A,Or(C,D)), Implies(B, Or(C,D))]).proof()

Out[20]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , : , :
1theorem
proveit.logic.boolean.disjunction.singularConstructiveDilemma
2assumption
3assumption
4assumption
5assumption
6assumption
In [21]:
Or(A,B,C,D).deriveViaDilemma(E,[Or(A,B,C,D),Implies(A,E), Implies(B,E), Implies(C,E), Implies(D,E), inBool(A) ,inBool(B),inBool(C),inBool(D)]).proof()

Out[21]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8
: , : , :
1theorem
proveit.logic.boolean.disjunction.singularConstructiveMultiDilemma
2theorem
proveit.number.numeral.deci.nat4
3specialization9, 10, 11, 12, 13
: , : , : , : , :
4assumption
5assumption
6assumption
7assumption
8assumption
9theorem
proveit.logic.set_theory.membership.exp_set_4
10assumption
11assumption
12assumption
13assumption
In [22]:
Or(A,B).prove([inBool(B), A, inBool(A)]).proof()

Out[22]:
step typerequirementsstatement
0specialization1, 2, 3, 4
: , :
1theorem
proveit.logic.boolean.disjunction.orIfLeft
2assumption
3assumption
4assumption
In [23]:
Or(A,B).prove([inBool(A), inBool(B), B]).proof()

Out[23]:
step typerequirementsstatement
0specialization1, 2, 3, 4
: , :
1theorem
proveit.logic.boolean.disjunction.orIfRight
2assumption
3assumption
4assumption
In [24]:
Or(C,D).deriveViaDilemma(Or(C,D),[Or(A,B), Or(C,D),Implies(A,C), Implies(A,C),Implies(B,D), inBool(A), inBool(B), inBool(C), inBool(D)]).proof()

Out[24]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , : , : , :
1theorem
proveit.logic.boolean.disjunction.constructiveDilemma
2assumption
3assumption
4assumption
5specialization7
:
6specialization7
:
7theorem
proveit.logic.boolean.implication.selfImplication
In [25]:
Or(A,B,C,D).deriveViaMultiDilemma(Or(H,I,J,K),[Or(A,B,C,D), Implies(A,H), Implies(B,I), Implies(C,J), Implies(D,K),inBool(A), inBool(B), inBool(C), inBool(D), inBool(H), inBool(I), inBool(J), inBool(K)]).proof()

Out[25]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12
: , : , :
1theorem
proveit.logic.boolean.disjunction.constructiveMultiDilemma
2theorem
proveit.number.numeral.deci.nat4
3specialization17, 13, 14, 15, 16
: , : , : , : , :
4assumption
5specialization17, 18, 19, 20, 21
: , : , : , : , :
6assumption
7assumption
8assumption
9assumption
10theorem
11theorem
12theorem
13assumption
14assumption
15assumption
16assumption
17theorem
proveit.logic.set_theory.membership.exp_set_4
18assumption
19assumption
20assumption
21assumption
In [26]:
Or(A,B,C,D).deriveViaDilemma(Or(H,I,J,K),[Or(A,B,C,D), Implies(A,H), Implies(B,I), Implies(C,J), Implies(D,K),inBool(A), inBool(B), inBool(C), inBool(D), inBool(H), inBool(I), inBool(J), inBool(K)]).proof()

Out[26]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12
: , : , :
1theorem
proveit.logic.boolean.disjunction.constructiveMultiDilemma
2theorem
proveit.number.numeral.deci.nat4
3specialization17, 13, 14, 15, 16
: , : , : , : , :
4assumption
5specialization17, 18, 19, 20, 21
: , : , : , : , :
6assumption
7assumption
8assumption
9assumption
10theorem
11theorem
12theorem
13assumption
14assumption
15assumption
16assumption
17theorem
proveit.logic.set_theory.membership.exp_set_4
18assumption
19assumption
20assumption
21assumption
In [27]:
Or(H, I, J, K).deducePartInBool(2, inBool(H,I,J,K)).proof()

Out[27]:
step typerequirementsstatement
0specialization1, 2, 3, 4
: , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.eachInBool
2theorem
proveit.number.numeral.deci.nat2
3theorem
proveit.number.numeral.deci.nat1
4specialization5, 6, 7, 8, 9, 10
: , :
5theorem
proveit.logic.boolean.disjunction.closure
6theorem
proveit.number.numeral.deci.nat4
7specialization11, 12, 13, 14, 15
: , : , : , : , :
8theorem
9theorem
10theorem
11theorem
proveit.logic.set_theory.membership.exp_set_4
12assumption
13assumption
14assumption
15assumption

destructiveDilemma

In [28]:
Or(Not(C),Not(D)).deriveViaDilemma(Or(Not(A),Not(B)),[Or(Not(C),Not(D)), Implies(A,C), Implies(B,D),inBool(A),inBool(B),inBool(C),inBool(D)]).proof()

Out[28]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8
: , : , : , :
1theorem
proveit.logic.boolean.disjunction.destructiveDilemma
2assumption
3assumption
4assumption
5assumption
6assumption
7assumption
8assumption
In [29]:
Or(Not(A), Not(B), Not(C), Not(D)).deriveViaDilemma(Or(Not(H), Not(I), Not(J), Not(K)),[Or(Not(A), Not(B), Not(C), Not(D)),Implies(A,H), Implies(B,I), Implies(C,J), Implies(D,K),inBool(A), inBool(B), inBool(C), inBool(D), inBool(H), inBool(I), inBool(J), inBool(K)]).proof()

Out[29]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12
: , : , :
1theorem
proveit.logic.boolean.disjunction.destructiveMultiDilemma
2theorem
proveit.number.numeral.deci.nat4
3specialization17, 13, 14, 15, 16
: , : , : , : , :
4assumption
5specialization17, 18, 19, 20, 21
: , : , : , : , :
6assumption
7assumption
8assumption
9assumption
10theorem
11theorem
12theorem
13assumption
14assumption
15assumption
16assumption
17theorem
proveit.logic.set_theory.membership.exp_set_4
18assumption
19assumption
20assumption
21assumption
In [30]:
Not(A).prove([Not(Or(A,B))]).proof()

Out[30]:
step typerequirementsstatement
0specialization1, 2
: , :
1theorem
proveit.logic.boolean.disjunction.notLeftIfNeither
2assumption
In [31]:
Not(B).prove([Not(Or(A,B))]).proof()

Out[31]:
step typerequirementsstatement
0specialization1, 2
: , :
1theorem
proveit.logic.boolean.disjunction.notRightIfNeither
2assumption
In [32]:
Or(A).deduceUnaryEquiv([inBool(A)]).proof()

Out[32]:
step typerequirementsstatement
0specialization1, 2
:
1theorem
proveit.logic.boolean.disjunction.unaryDisjunctionDef
2assumption
In [33]:
inBool(B).prove([inBool(Or(A,B,C))]).proof()

Out[33]:
step typerequirementsstatement
0specialization1, 2, 3
: , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.eachInBool
2theorem
proveit.number.numeral.deci.nat1
3assumption
In [34]:
Or(A,B,C).prove([A,inBool(A),inBool(B),inBool(C)]).proof()

Out[34]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8
: , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.orIfAny
2theorem
proveit.number.sets.integer.zeroInNats
3theorem
proveit.number.numeral.deci.nat2
4specialization9, 10
: , :
5assumption
6assumption
7specialization11, 12, 13
: , : , :
8theorem
9theorem
proveit.logic.set_theory.membership.exp_set_0
10axiom
proveit.number.sets.integer.listLen0
11theorem
proveit.logic.set_theory.membership.exp_set_2
12assumption
13assumption
In [35]:
Not(Or(A,B,C)).prove([Not(A), Not(B), Not(C)]).proof()

Out[35]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7
: , :
1theorem
proveit.logic.boolean.disjunction.notOrIfNotAny
2theorem
proveit.number.numeral.deci.nat3
3assumption
4assumption
5assumption
6theorem
7theorem
In [36]:
Or(A,B,C).deriveContradiction([Or(A,B,C), Not(A), Not(B), Not(C)]).proof()

Out[36]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , :
1theorem
2theorem
proveit.number.numeral.deci.nat3
3assumption
4assumption
5assumption
6assumption
In [37]:
groupCD = Or(A,B,C,D,E,F,G).associate(2,length=2,assumptions=[Or(A,B,Or(C,D),E,F,G),Or(A,B,C,D,E,F,G),inBool(A), inBool(B),inBool(C),inBool(D),inBool(E),inBool(F),inBool(G)])

Out[37]:
groupCD:
In [38]:
groupCD.proof()

Out[38]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.associate
2theorem
proveit.number.numeral.deci.nat2
3theorem
proveit.number.numeral.deci.nat3
4assumption
5theorem
6theorem
In [39]:
groupCD.disassociate(2, assumptions=[groupCD.expr]).proof()

Out[39]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.disassociate
2theorem
proveit.number.numeral.deci.nat2
3theorem
proveit.number.numeral.deci.nat3
4assumption
5theorem
6theorem
In [40]:
Or(A,B,C,D,E).commutation(1,3, inBool(A,B,C,D,E)).proof()

Out[40]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8
: , : , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.rightwardCommutation
2theorem
proveit.number.numeral.deci.nat1
3theorem
proveit.number.numeral.deci.nat2
4specialization13, 9
: , :
5assumption
6specialization10, 11, 12
: , : , :
7specialization13, 14
: , :
8theorem
9assumption
10theorem
proveit.logic.set_theory.membership.exp_set_2
11assumption
12assumption
13theorem
proveit.logic.set_theory.membership.exp_set_1
14assumption
In [41]:
Or(A,B,C,D,E).commutation(-1,0, inBool(A,B,C,D,E)).proof()

Out[41]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8, 9
: , : , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.leftwardCommutation
2theorem
proveit.number.sets.integer.zeroInNats
3theorem
proveit.number.numeral.deci.nat4
4specialization10, 11
: , :
5specialization12, 13, 14, 15, 16
: , : , : , : , :
6assumption
7theorem
8theorem
9theorem
10theorem
proveit.logic.set_theory.membership.exp_set_0
11axiom
proveit.number.sets.integer.listLen0
12theorem
proveit.logic.set_theory.membership.exp_set_4
13assumption
14assumption
15assumption
16assumption
In [42]:
Or(A,B,C,D,E,F,G,H,I).commute(3, 5, [Or(A,B,C,D,E,F,G,H,I), *inBool(A,B,C,D,E,F,G,H,I)]).proof()

Out[42]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , : , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.rightwardCommute
2theorem
proveit.number.numeral.deci.nat3
3theorem
proveit.number.numeral.deci.nat2
4assumption
5theorem
6theorem
In [43]:
Or(A,B,C,D,E,F,G,H,I).commute(6, 3, [Or(A,B,C,D,E,F,G,H,I), *inBool(A,B,C,D,E,F,G,H,I)]).proof()

Out[43]:
step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6
: , : , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.leftwardCommute
2theorem
proveit.number.numeral.deci.nat3
3theorem
proveit.number.numeral.deci.nat2
4assumption
5theorem
6theorem
In [44]:
Or(A,B,C,D,E,F,G,H,I).groupCommute(0, 3, length=2, assumptions=[Or(A,B,C,D,E,F,G,H,I), *inBool(A,B,C,D,E,F,G,H,I)]).proof()

Out[44]:
step typerequirementsstatement
0specialization1, 4, 9, 5, 2, 12, 13, 14
: , : , : , : , : , :
1theorem
proveit.logic.boolean.disjunction.disassociate
2specialization3, 8, 4, 5, 6, 12, 13, 14
: , : , : , : , : , : , :
3theorem
proveit.logic.boolean.disjunction.rightwardCommute
4theorem
proveit.number.numeral.deci.nat3
5theorem
proveit.number.numeral.deci.nat4
6specialization7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17
: , : , : , : , : , :
7theorem
proveit.logic.boolean.disjunction.associate
8theorem
proveit.number.sets.integer.zeroInNats
9theorem
proveit.number.numeral.deci.nat2
10theorem
proveit.number.numeral.deci.nat7
11assumption
12theorem
13theorem
14theorem
15theorem
16theorem
17theorem
In [45]:
Or(A,B,C,D).groupCommute(0, 1, length=2, assumptions=[Or(A,B,C,D)])

Out[45]:
In [46]:
Or(A,B,C,D).groupCommutation(0, 1, length=2, assumptions=inBool(A,B,C,D))

Out[46]:
In [47]:
And(A, B, Or(A,B,C,D)).innerExpr().operands[2].groupCommutation(0, 1, length=2, assumptions=inBool(A,B,C,D)).proof()

Out[47]:
step typerequirementsstatement
0specialization1, 2
: , : , :
1axiom
proveit.logic.equality.substitution
2specialization5, 3, 4
: , : , :
3specialization5, 6, 7
: , : , :
4specialization8, 16, 10, 19, 11, 20, 13
: , : , : , : , : , :
5axiom
proveit.logic.equality.equalsTransitivity
6specialization9, 15, 10, 17, 11, 12, 13
: , : , : , : , : , :
7specialization14, 15, 16, 17, 18, 19, 20
: , : , : , : , : , : , :
8theorem
proveit.logic.boolean.disjunction.disassociation
9theorem
proveit.logic.boolean.disjunction.association
10theorem
proveit.number.numeral.deci.nat2
11specialization21, 25, 26
: , : , :
12specialization21, 27, 29
: , : , :
13theorem
14theorem
proveit.logic.boolean.disjunction.rightwardCommutation
15theorem
proveit.number.sets.integer.zeroInNats
16theorem
proveit.number.numeral.deci.nat1
17specialization22, 23
: , :
18specialization24, 25, 26
: , :
19specialization28, 27
: , :
20specialization28, 29
: , :
21theorem
proveit.logic.set_theory.membership.exp_set_2
22theorem
proveit.logic.set_theory.membership.exp_set_0
23axiom
proveit.number.sets.integer.listLen0
24theorem
proveit.logic.boolean.disjunction.binaryClosure
25assumption
26assumption
27assumption
28theorem
proveit.logic.set_theory.membership.exp_set_1
29assumption
In [48]:
And(A, B, Or(A,B,C,D)).innerExpr().operands[2].groupCommute(0, 1, length=2, assumptions=[And(A, B, Or(A,B,C,D))]).proof()

Out[48]:
step typerequirementsstatement
0specialization1, 36, 2
: , : , :
1theorem
proveit.logic.equality.subRightSideInto
2specialization5, 3, 4
: , : , :
3specialization5, 6, 7
: , : , :
4specialization8, 27, 32, 16, 10, 17, 12
: , : , : , : , : , :
5axiom
proveit.logic.equality.equalsTransitivity
6specialization9, 33, 32, 14, 10, 11, 12
: , : , : , : , : , :
7specialization13, 33, 27, 14, 15, 16, 17
: , : , : , : , : , : , :
8theorem
proveit.logic.boolean.disjunction.disassociation
9theorem