Conditional Properties
In each statement, if the test expression is true, then the conclusion expression is also assumed to be true. Conditional properties are used to prove theorems.
if height of tree left = height of tree right, then height of tree (node (v, left, right)) = (height of tree left) + 1
if the following are true:
- height of tree (node (lv, ll, lr)) > (height of tree right) + 1
- height of tree ll > height of tree lr
then result of balancing the tree (node (v, (node (lv, ll, lr)), right)) = result of rotating (node (v, (node (lv, ll, lr)), right)) clockwise
if the following are true:
- height of tree (node (lv, ll, lr)) > (height of tree right) + 1
- height of tree ll < height of tree lr
then result of balancing the tree (node (v, (node (lv, ll, lr)), right)) = result of rotating (node (v, (node (lv, ll, lr)), right)) twice
if val < a, then output of the bst_delete function where input tree is (node (a, left, right)), value is val, visited is visited, and moves are moves = output of the bst_delete function where input tree is left, value is val, visited is [ node (a, None, right), visited ], and moves are [ "L", moves ]
if val > a, then output of the bst_delete function where input tree is (node (a, left, right)), value is val, visited is visited, and moves are moves = output of the bst_delete function where input tree is right, value is val, visited is [ node (a, left, None), visited ], and moves are [ "R", moves ]
if val = b, then output of the bst_delete function where input tree is (node (a, (node (b, None, (node (c, cl, cr)))), right)), value is val, visited is visited, and moves are moves = result of building the BST from nodes [ node (a, (node (c, cl, cr)), right), visited ] and moves moves
if the following are true:
- val = a
- tree = node (a, (node (l, ll, lr)), (node (r, rl, rr)))
- smallest value in (node (r, rl, rr)) = near
then output of the bst_delete function where input tree is tree, value is val, visited is visited, and moves are moves = result of building the BST from nodes [ result of updating the root of (result of removing near from tree tree) with near, visited ] and moves moves
if xp = z, then logxz = p
if logxz = p, then xp = z
if M is the midpoint of line AB, then point M is in segment AB
if m∠ABC = 180, then point B is in segment AC
if point M is in segment AB, then point M lies in interior of ∠AXB
if AB || CD, then point C lies in interior of ∠ABD
if m∠ABC = 180, then point X lies in interior of ∠ABC
if (point M is in segment BC) and (m∠AME = 180) and (m∠ACD = 180), then point E lies in interior of ∠BCD
if ray BX bisects ∠ABC, then point X lies in interior of ∠ABC
if ((m∠ABX) + (m∠XBC) = 180) or ((m∠ABX) + (m∠XBC) < 180), then point X lies in interior of ∠ABC
if point X lies in interior of ∠ABC, then ((m∠ABX) + (m∠XBC) < 180) or ((m∠ABX) + (m∠XBC) = 180)
if ((m∠ABX) + (m∠XBC) < 180) or ((m∠ABX) + (m∠XBC) = 180), then m∠ABC = (m∠ABX) + (m∠XBC)
if AB ⊥ BC, then ∠ABC is a right angle
if ∠ABC is a right angle, then AB ⊥ BC
if ∠ABC is a right angle, then △ABC is a right triangle
if △ABC is a right triangle, then ∠ABC is a right angle
if ∠ABC is a right angle, then m∠ABC = 90
if m∠ABC = 90, then ∠ABC is a right angle
if (△XYZ is a triangle) and (segment XY ≅ segment YZ), then △XYZ is an isosceles triangle
if ray BD bisects ∠ABC, then m∠ABD = m∠DBC
if m∠ABD = m∠DBC, then ray BD bisects ∠ABC
if ray BD bisects ∠ABC, then m∠DBC = (m∠ABC) / 2
if (ray BD bisects ∠ABC) and (m∠BPD = 180) and (PM ⊥ MB) and (PN ⊥ NB), then distance PM = distance PN
if (distance PM = distance PN) and (PM ⊥ MB) and (PN ⊥ NB), then ray BP bisects ∠ABC
if (∠ABC is an acute angle) and (∠BCA is an acute angle) and (∠CAB is an acute angle), then △ABC is an acute triangle
if ∠ABC is an acute angle, then m∠ABC < 90
if m∠ABC = 180, then (distance AB) + (distance BC) = distance AC
if m∠ABC = 180, then m∠BCX = m∠ACX
if m∠ABC = 180, then m∠ABC = (m∠ABX) + (m∠XBC)
if M is the midpoint of line AB, then distance AM = distance MB
if (distance AM = distance MB) and (m∠AMB = 180), then M is the midpoint of line AB
if M is the midpoint of line AB, then m∠AMB = 180
if M is the midpoint of line AB, then the x coordinate of point M = ((the x coordinate of point A) + (the x coordinate of point B)) / 2
if M is the midpoint of line AB, then the y coordinate of point M = ((the y coordinate of point A) + (the y coordinate of point B)) / 2
if ∠ABC and ∠DEF are complementary, then (m∠ABC) + (m∠DEF) = 90
if ∠ABC and ∠DEF are supplementary, then (m∠ABC) + (m∠DEF) = 180
if (m∠ABC) + (m∠DEF) = 180, then ∠ABC and ∠DEF are supplementary
if m∠CDE = m∠CAB, then DE || AB
if (AB || CD) and (∠ABD is a right angle), then ∠BDC is a right angle
if AB || CD, then BA || DC
if AB || CD, then CD || AB
if (AB || YZ) and (m∠ABC = 180), then BC || YZ
if (AB || YZ) and (m∠AXB = 180), then AX || YZ
if (AB || YZ) and (m∠ABC = 180) and (m∠XYZ = 180), then AC || XZ
if (AB || XY) and (m∠ABC = 180) and (m∠XYZ = 180), then AC || XZ
if (AC || XZ) and (m∠ABC = 180) and (m∠XYZ = 180), then AB || YZ
if (AC || XZ) and (m∠ABC = 180) and (m∠XYZ = 180), then AB || XY
if (AB || CD) and (m∠AXB = 180) and (m∠CYD = 180), then XB || CY
if (AB || CD) and (m∠AXY = 180) and (m∠XYB = 180), then XY || CD
if ABCD is a square, then ABCD is a rectangle
if ABCD is a square, then distance AB = distance BC
if (ABCD is a rectangle) and (distance AB = distance BC), then ABCD is a square
if m∠abc = 90, then area of △ABC = (((distance AB) ⋅ (distance BC)) ⋅ 1) / 2
if AB || CD, then not(line AB intersects line CD)
if AB || CD, then (m∠BAC) + (m∠ACD) = 180
if (m∠BAC) + (m∠ACD) = 180, then AB || CD
if (m∠DBA) + (m∠CDB) = 180, then AB || CD
if △ABC ≅ △DEF, then area of △ABC = area of △DEF
if △ABC ≅ △DEF, then △BCA ≅ △EFD
if △ABC ≅ △DEF, then △BAC ≅ △EDF
if △ABC ≅ △DEF, then △DEF ≅ △ABC
if (△ABC ≅ △DEF) and (△DEF ≅ △GHI), then △ABC ≅ △GHI
if (distance AB = distance DE) and (m∠ABC = m∠DEF) and (distance BC = distance EF), then area of △ABC = area of △DEF
if (distance AB = distance DE) and (m∠ABC = m∠DEF) and (distance BC = distance EF), then △ABC ≅ △DEF
if (m∠ABC = m∠DEF) and (distance BC = distance EF) and (m∠BCA = m∠EFD), then △ABC ≅ △DEF
if (distance AB = distance DE) and (distance BC = distance EF) and (distance CA = distance FD), then △ABC ≅ △DEF
if (m∠ABC = m∠DEF) and (distance BC = distance EF) and (m∠BCA = m∠EFD), then area of △ABC = area of △DEF
if △ABC ≅ △DEF, then m∠ABC = m∠DEF
if △ABC ≅ △DEF, then m∠CAB = m∠FDE
if △ABC ≅ △DEF, then m∠BCA = m∠EFD
if △ABC ≅ △DEF, then distance AB = distance DE
if △ABC ≅ △DEF, then distance BC = distance EF
if △ABC ≅ △DEF, then distance CA = distance FD
if (distance AB = distance BC) and (distance BC = distance CD) and (distance CD = distance DA) and (m∠ABC = 90), then ABCD is a square
if ABCD is a square, then area of quadrilateral ABCD = (distance AB) ⋅ (distance AB)
if m∠ABC = 180, then area of △ACD = area of quadrilateral ABCD
if m∠ABC = 180, then area of quadrilateral XABC = area of △XAC
if m∠ABC = 180, then area of pentagon ACDEF = area of hexagon ABCDEF
if m∠DEF = 180, then area of hexagon ABCDEF = area of pentagon ABCDF
if (m∠ABC = 90) and (m∠DEF = 180), then m∠ABC < m∠DEF
if line AB intersects line CD at point X, then m∠AXB = 180
if line AB intersects line CD at point X, then m∠CXD = 180
if (m∠ABD = 180) and (m∠ACD = 180), then m∠ABC = 180
if (m∠ABD = 180) and (m∠ACD = 180), then m∠BCD = 180
if (m∠ABC = 180) and (m∠BCD = 180), then m∠ABD = 180
if (m∠ABC = 180) and (m∠BCD = 180), then m∠ACD = 180
if (AB || CD) and (line AB intersects line EF at point X), then line EF intersects line CD at point Z
if (AB || CD) and (AC || BD), then ABDC is a parallelogram
if ABCD is a parallelogram, then AB || DC
if ABCD is a parallelogram, then AD || BC
if ABCD is a rectangle, then ABCD is a parallelogram
if ABCD is a rectangle, then ∠ABC is a right angle
if (ABCD is a parallelogram) and (∠ABC is a right angle), then ABCD is a rectangle