logo

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 ⊢ 
 proveit.number.numeral.deci.add_1_1
5theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
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 ⊢ 
 proveit.logic.boolean.disjunction.binaryOrContradiction
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
11theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
12theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
11theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
12theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
9theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
10theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
11theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
12theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
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, 9 ⊢ 
  : , : , : , : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.orIfAny
2theorem ⊢ 
 proveit.number.sets.integer.zeroInNats
3theorem ⊢ 
 proveit.number.numeral.deci.nat2
4specialization10, 11 ⊢ 
  : , :
5assumption ⊢ 
6assumption ⊢ 
7specialization12, 13, 14 ⊢ 
  : , : , :
8theorem ⊢ 
 proveit.number.numeral.deci.less_0_1
9theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
10theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_0
11axiom ⊢ 
 proveit.number.sets.integer.listLen0
12theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_2
13assumption ⊢ 
14assumption ⊢ 
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
7theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
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 ⊢ 
 proveit.logic.boolean.disjunction.orContradiction
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
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, 10 ⊢ 
  : , : , : , : , : , : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.leftwardCommutation
2theorem ⊢ 
 proveit.number.sets.integer.zeroInNats
3theorem ⊢ 
 proveit.number.numeral.deci.nat4
4specialization11, 12 ⊢ 
  : , :
5specialization13, 14, 15, 16, 17 ⊢ 
  : , : , : , : , :
6assumption ⊢ 
7theorem ⊢ 
 proveit.number.numeral.deci.less_0_1
8theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
9theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
10theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
11theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_0
12axiom ⊢ 
 proveit.number.sets.integer.listLen0
13theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_4
14assumption ⊢ 
15assumption ⊢ 
16assumption ⊢ 
17assumption ⊢ 
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
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 ⊢ 
 proveit.number.numeral.deci.add_1_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
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, 13, 14, 15 ⊢ 
  : , : , : , : , : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.disassociate
2specialization3, 8, 4, 5, 6, 12, 13, 14, 15 ⊢ 
  : , : , : , : , : , : , :
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, 18 ⊢ 
  : , : , : , : , : , :
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 ⊢ 
 proveit.number.numeral.deci.less_0_1
13theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
14theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
15theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
16theorem ⊢ 
 proveit.number.numeral.deci.add_4_1
17theorem ⊢ 
 proveit.number.numeral.deci.add_5_1
18theorem ⊢ 
 proveit.number.numeral.deci.add_6_1
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, 21, 13 ⊢ 
  : , : , : , : , : , :
7specialization14, 15, 16, 17, 18, 19, 20, 21 ⊢ 
  : , : , : , : , : , : , :
8theorem ⊢ 
 proveit.logic.boolean.disjunction.disassociation
9theorem ⊢ 
 proveit.logic.boolean.disjunction.association
10theorem ⊢ 
 proveit.number.numeral.deci.nat2
11specialization22, 26, 27 ⊢ 
  : , : , :
12specialization22, 28, 30 ⊢ 
  : , : , :
13theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
14theorem ⊢ 
 proveit.logic.boolean.disjunction.rightwardCommutation
15theorem ⊢ 
 proveit.number.sets.integer.zeroInNats
16theorem ⊢ 
 proveit.number.numeral.deci.nat1
17specialization23, 24 ⊢ 
  : , :
18specialization25, 26, 27 ⊢ 
  : , :
19specialization29, 28 ⊢ 
  : , :
20specialization29, 30 ⊢ 
  : , :
21theorem ⊢ 
 proveit.number.numeral.deci.less_0_1
22theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_2
23theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_0
24axiom ⊢ 
 proveit.number.sets.integer.listLen0
25theorem ⊢ 
 proveit.logic.boolean.disjunction.binaryClosure
26assumption ⊢ 
27assumption ⊢ 
28assumption ⊢ 
29theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_1
30assumption ⊢ 
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, 37, 2 ⊢ 
  : , : , :
1theorem ⊢ 
 proveit.logic.equality.subRightSideInto
2specialization5, 3, 4 ⊢ 
  : , : , :
3specialization5, 6, 7 ⊢ 
  : , : , :
4specialization8, 28, 33, 16, 10, 17, 12 ⊢ 
  : , : , : , : , : , :
5axiom ⊢ 
 proveit.logic.equality.equalsTransitivity
6specialization9, 34, 33, 14, 10, 11, 18, 12 ⊢ 
  : , : , : , : , : , :
7specialization13, 34, 28, 14, 15, 16, 17, 18 ⊢ 
  : , : , : , : , : , : , :
8theorem ⊢ 
 proveit.logic.boolean.disjunction.disassociation
9theorem ⊢ 
 proveit.logic.boolean.disjunction.association
10specialization19, 23, 24 ⊢ 
  : , : , :
11specialization19, 25, 27 ⊢ 
  : , : , :
12theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
13theorem ⊢ 
 proveit.logic.boolean.disjunction.rightwardCommutation
14specialization20, 21 ⊢ 
  : , :
15specialization22, 23, 24 ⊢ 
  : , :
16specialization26, 25 ⊢ 
  : , :
17specialization26, 27 ⊢ 
  : , :
18theorem ⊢ 
 proveit.number.numeral.deci.less_0_1
19theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_2
20theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_0
21axiom ⊢ 
 proveit.number.sets.integer.listLen0
22theorem ⊢ 
 proveit.logic.boolean.disjunction.binaryClosure
23specialization32, 34, 33, 35 ⊢ 
  : , : , : , : , :
24specialization32, 28, 35 ⊢ 
  : , : , : , : , :
25specialization29, 33, 28, 31 ⊢ 
  : , : , : , : , :
26theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_1
27specialization29, 30, 34, 31 ⊢ 
  : , : , : , : , :
28theorem ⊢ 
 proveit.number.numeral.deci.nat1
29theorem ⊢ 
 proveit.logic.boolean.disjunction.eachInBool
30theorem ⊢ 
 proveit.number.numeral.deci.nat3
31specialization32, 33, 34, 35 ⊢ 
  : , : , : , : , :
32theorem ⊢ 
 proveit.logic.boolean.conjunction.eachInBool
33theorem ⊢ 
 proveit.number.numeral.deci.nat2
34theorem ⊢ 
 proveit.number.sets.integer.zeroInNats
35specialization36, 37 ⊢ 
  :
36theorem ⊢ 
 proveit.logic.boolean.inBoolIfTrue
37assumption ⊢ 
In [49]:
Or(A,B,C,D,E,F,G,H).deriveInBool(inBool(A,B,C,D,E,F,G,H)).proof()
Out[49]:
 step typerequirementsstatement
0specialization1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ⊢ 
  : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.closure
2theorem ⊢ 
 proveit.number.numeral.deci.nat8
3specialization11, 12, 13, 14, 15, 16, 17, 18, 19 ⊢ 
  : , : , : , : , : , : , : , : , :
4theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
5theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
7theorem ⊢ 
 proveit.number.numeral.deci.add_4_1
8theorem ⊢ 
 proveit.number.numeral.deci.add_5_1
9theorem ⊢ 
 proveit.number.numeral.deci.add_6_1
10theorem ⊢ 
 proveit.number.numeral.deci.add_7_1
11theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_8
12assumption ⊢ 
13assumption ⊢ 
14assumption ⊢ 
15assumption ⊢ 
16assumption ⊢ 
17assumption ⊢ 
18assumption ⊢ 
19assumption ⊢ 

trueEval

In [50]:
Or(FALSE,FALSE,TRUE,FALSE,FALSE).evaluation().proof()
Out[50]:
 step typerequirementsstatement
0specialization1, 2 ⊢ 
  :
1axiom ⊢ 
 proveit.logic.boolean.eqTrueIntro
2specialization3, 4, 5, 6, 7, 8 ⊢ 
  : , : , : , : , :
3theorem ⊢ 
 proveit.logic.boolean.disjunction.orIfAny
4theorem ⊢ 
 proveit.number.numeral.deci.nat2
5specialization9, 10 ⊢ 
  : , : , :
6theorem ⊢ 
 proveit.logic.boolean.trueInBool
7axiom ⊢ 
 proveit.logic.boolean.trueAxiom
8theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
9theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_2
10theorem ⊢ 
 proveit.logic.boolean.falseInBool
In [51]:
Or(A,B,TRUE,C,D).evaluation([inBool(A), inBool(B), inBool(C), inBool(D)]).proof()
Out[51]:
 step typerequirementsstatement
0specialization1, 2 ⊢ 
  :
1axiom ⊢ 
 proveit.logic.boolean.eqTrueIntro
2specialization3, 4, 5, 6, 7, 8, 9 ⊢ 
  : , : , : , : , :
3theorem ⊢ 
 proveit.logic.boolean.disjunction.orIfAny
4theorem ⊢ 
 proveit.number.numeral.deci.nat2
5specialization12, 10, 11 ⊢ 
  : , : , :
6theorem ⊢ 
 proveit.logic.boolean.trueInBool
7axiom ⊢ 
 proveit.logic.boolean.trueAxiom
8specialization12, 13, 14 ⊢ 
  : , : , :
9theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
10assumption ⊢ 
11assumption ⊢ 
12theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_2
13assumption ⊢ 
14assumption ⊢ 

falseEval

In [52]:
Equals(Or(A,B,C,D),FALSE).prove([Equals(A,FALSE), Equals(B,FALSE),Equals(C,FALSE),Equals(D,FALSE)]).proof()
Out[52]:
 step typerequirementsstatement
0specialization1, 2 ⊢ 
  :
1axiom ⊢ 
 proveit.logic.boolean.negation.negationElim
2specialization3, 4, 5, 6, 7, 8, 9, 10, 11 ⊢ 
  : , :
3theorem ⊢ 
 proveit.logic.boolean.disjunction.notOrIfNotAny
4theorem ⊢ 
 proveit.number.numeral.deci.nat4
5specialization15, 12 ⊢ 
  :
6specialization15, 13 ⊢ 
  :
7specialization15, 14 ⊢ 
  :
8specialization15, 16 ⊢ 
  :
9theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
10theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
11theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
12assumption ⊢ 
13assumption ⊢ 
14assumption ⊢ 
15axiom ⊢ 
 proveit.logic.boolean.negation.negationIntro
16assumption ⊢ 
In [53]:
inBool(Or(A,B)).prove([inBool(A), inBool(B)]).proof()
Out[53]:
 step typerequirementsstatement
0specialization1, 2, 3 ⊢ 
  : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.binaryClosure
2assumption ⊢ 
3assumption ⊢ 
In [54]:
inBool(Or(A,B,C,D)).prove([inBool(A), inBool(B), inBool(C), inBool(D)]).proof()
Out[54]:
 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 ⊢ 
 proveit.number.numeral.deci.add_1_1
5theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
6theorem ⊢ 
 proveit.number.numeral.deci.add_3_1
7theorem ⊢ 
 proveit.logic.set_theory.membership.exp_set_4
8assumption ⊢ 
9assumption ⊢ 
10assumption ⊢ 
11assumption ⊢ 
In [55]:
Or(A,B).prove([Not(And(Not(A), Not(B)))]).proof()
Out[55]:
 step typerequirementsstatement
0specialization1, 2 ⊢ 
  : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.demorgansLawAndToOrBin
2assumption ⊢ 
In [56]:
Or(A, B, C).prove([Not(And(Not(A),Not(B),Not(C)))]).proof()
Out[56]:
 step typerequirementsstatement
0specialization1, 2, 3, 4, 5 ⊢ 
  : , :
1theorem ⊢ 
 proveit.logic.boolean.disjunction.demorgansLawAndToOr
2theorem ⊢ 
 proveit.number.numeral.deci.nat3
3assumption ⊢ 
4theorem ⊢ 
 proveit.number.numeral.deci.add_1_1
5theorem ⊢ 
 proveit.number.numeral.deci.add_2_1
In [57]:
%end demonstrations