Proofs
A proof is a series of claims that lead to a conclusion. Some proofs are conditional, which means that the claims can only be made under certain conditions. Click on a statement to see the proof
if m∠DAX = m∠XBC and m∠AXB = 180, then m∠DAB = m∠ABC
if m∠ABC = 180 and m∠IJK = 180 and m∠XCA = m∠YKI, then m∠XCB = m∠YKJ
if m∠AMB = 180, then ∠AMC and ∠BMC are supplementary
if ∠ABC and ∠DEF are supplementary, then (m∠ABC) + (m∠FED) = 180
if ∠ABC is a right angle, then m∠CBA = 90
if ∠ABC is a right angle and ∠DEF is a right angle, then m∠ABC = m∠DEF
if ∠ABC is a right angle, then ∠CBA is a right angle
if m∠BDA = 180 and m∠CEA = 180, then m∠BAE = m∠CAD
if m∠ABC = 180, then m∠XAB = m∠XAC
if AB ⊥ BC, then m∠ABC = 90
if m∠ABC = 90, then AB ⊥ BC
if △ABC is a right triangle, then m∠ABC = 90
if △ABC ≅ △DEF, then distance BA = distance ED
if △ABC ≅ △DEF, then distance CB = distance FE
if △ABC ≅ △DEF, then distance AC = distance DF
if △ABC ≅ △DEF, then m∠BAC = m∠FDE
if △ABC ≅ △DEF, then m∠EFD = m∠ACB
if AB || CD, then DC || BA
if AB || CD and DB || CA, then ABDC is a parallelogram
if △ABC ∼ △DEF, then (distance AB) / (distance DE) = (distance AC) / (distance DF)
if △ABC ∼ △XYZ, then (distance CB) / (distance ZY) = (distance BA) / (distance YX)
(distance AB) / (distance CD) = (distance BA) / (distance DC)
if m∠ABC = 180 and m∠XBA = 90, then m∠XBC = 90
if M is the midpoint of line AB, then distance AM = distance BM
if M is the midpoint of line AB, then distance AB = (distance AM) ⋅ 2
if M is the midpoint of line AB, then (distance MB) ⋅ 2 = distance AB
if M is the midpoint of line AB, then distance AB = (distance MB) ⋅ 2
if M is the midpoint of line AB, then (distance BM) ⋅ 2 = distance BA
if M is the midpoint of line AB, then distance MB = (distance AB) / 2
if M is the midpoint of line AB, then distance AM = (distance AB) / 2
if M is the midpoint of line AB, then (m∠AMX) + (m∠XMB) = 180
if x ⋅ (distance AB) = z, then x ⋅ (distance BA) = z
if x ⋅ (distance AB) = (distance CD) ⋅ y, then x ⋅ (distance BA) = (distance DC) ⋅ y
if x = (distance AB) + (distance CD), then x = (distance DC) + (distance AB)
if m∠ABC = 180, then (distance AC) + ((distance BC) ⋅ (-1)) = distance AB
if m∠ABC = 180, then (distance CA) + ((distance BC) ⋅ (-1)) = distance AB
if m∠ABC = 180, then (distance CA) + ((distance CB) ⋅ (-1)) = distance BA
if m∠ACF = (m∠ACG) + (m∠GCF), then m∠FCA = (m∠FCG) + (m∠GCA)
if distance AB > distance CD, then distance AB > distance DC
if m∠BAC > m∠CDB, then m∠CAB > m∠CDB
if point X lies in interior of ∠ABC, then m∠ABC = (m∠ABX) + (m∠XBC)
if point X lies in interior of ∠ABC, then (m∠ABX) + (m∠XBC) = m∠ABC
if m∠CAB > m∠CDB and m∠ABD = 180, then m∠CAD > m∠CDA
if (((m∠ABC) + (m∠BCA)) + (m∠CAB)) + (((m∠ACD) + (m∠CDA)) + (m∠DAC)) = (((((m∠ABC) + (m∠BCA)) + (m∠CAB)) + (m∠ACD)) + (m∠CDA)) + (m∠DAC), then (((m∠ABC) + (m∠BCA)) + (m∠CAB)) + (((m∠ACD) + (m∠CDA)) + (m∠DAC)) = (((m∠ABC) + (m∠CDA)) + ((m∠BCA) + (m∠ACD))) + ((m∠DAC) + (m∠CAB))
if △ABC ≅ △GEF and △DEF ≅ △GEF, then △ABC ≅ △DEF
if distance AB = distance DE and distance BC = distance EF and distance AC = distance DF, then △ABC ≅ △DEF
if x + (m∠ABC) = y, then x + (m∠CBA) = y
if m∠AXC = 180 and m∠DCA = m∠CAB, then m∠DCX = m∠XAB
if m∠BXD = 180 and m∠ADX = m∠CDX, then m∠ADB = m∠CDB
if m∠DBX = m∠CAY and m∠AXB = 180 and m∠AYB = 180, then m∠DBA = m∠CAB
if m∠DXY = 90 and m∠DXY = m∠DXB, then m∠BXD = 90
(distance BC) ⋅ (distance BC) = (distance CB) ⋅ (distance CB)
if (distance BC) ⋅ (distance BC) = ((distance AB) ⋅ (distance AB)) + ((distance AC) ⋅ (distance AC)), then (distance CB) ⋅ (distance CB) = ((distance CA) ⋅ (distance CA)) + ((distance AB) ⋅ (distance AB))
if tangent of (m∠BCA) = (distance AB) / (distance BC), then tangent of (m∠BCA) = (distance BA) / (distance CB)
if ∠ABC is a right angle, then tangent of (m∠BAC) = (distance CB) / (distance BA)
if ∠ABC is a right angle, then tangent of (m∠BAC) = (distance BC) / (distance AB)
if ∠ABC is a right angle, then tangent of (m∠CAB) = (distance BC) / (distance AB)
if ∠ABC is a right angle, then tangent of (m∠CAB) = (distance CB) / (distance AB)
if ∠ABC is a right angle, then sine of (m∠BAC) = (distance CB) / (distance CA)
if ∠ABC is a right angle, then sine of (m∠CAB) = (distance CB) / (distance CA)
if ∠ABC is a right angle, then sine of (m∠CAB) = (distance BC) / (distance AC)
if ∠ABC is a right angle, then sine of (m∠ACB) = (distance AB) / (distance AC)
if ∠ABC is a right angle, then cosine of (m∠BAC) = (distance BA) / (distance CA)
if ∠ABC is a right angle, then cosine of (m∠CAB) = (distance BA) / (distance CA)
if ∠ABC is a right angle, then cosine of (m∠CAB) = (distance BA) / (distance AC)
if ∠ABC is a right angle, then cosine of (m∠CAB) = (distance AB) / (distance AC)
if △ABC is an equilateral triangle, then distance BC = distance AC
if △ABC is an equilateral triangle, then distance AC = distance BC
if △ABC is an equilateral triangle, then distance CA = distance AB
if (distance AB) / (distance CB) = (distance BX) / (distance BA) and (distance AC) / (distance BC) = (distance CX) / (distance CA), then ((distance AB) ⋅ (distance AB)) + ((distance AC) ⋅ (distance AC)) = ((distance BC) ⋅ (distance BX)) + ((distance BC) ⋅ (distance CX))
if m∠XZE = 180, then m∠ZYX < m∠YZE
if m∠EZX = 180, then m∠EZY > m∠ZYX
if m∠XZE = 180, then m∠YZE > m∠YXZ
if m∠EZX = 180, then m∠YZE > m∠YXZ
if m∠XEY = 180, then m∠ZEY > m∠YXZ
if distance XY > distance YZ, then m∠XZY > m∠YXZ
if distance YZ < distance XY, then m∠YXZ < m∠XZY
if distance YZ < distance YX, then m∠YXZ < m∠XZY
if m∠ZXY > m∠XYZ, then distance ZY > distance ZX
if m∠ZXY > m∠ZYX, then distance ZY > distance ZX
if distance XZ = distance YZ and m∠XYP = 180, then distance ZP > distance ZX
if distance WX = distance YZ and m∠WXY = 180 and m∠XYZ = 180, then distance WY = distance XZ
if M is the midpoint of line XY, then distance XM = (distance XY) ⋅ (1 / 2)
if ∠AXB and ∠BXC are complementary and ∠BXC and ∠CXD are complementary, then m∠AXB = m∠CXD
if ∠AXB and ∠BXC are supplementary and ∠DXC and ∠BXC are supplementary, then m∠AXB = m∠DXC
if m∠XPW = 180 and m∠YPZ = 180, then m∠WPZ = m∠XPY
if m∠XPW = 180 and m∠YPZ = 180, then m∠YPX = m∠WPZ
if m∠XPW = 180 and m∠YPZ = 180, then m∠XPY = m∠WPZ
if m∠WPY = 180 and m∠XPZ = 180, then m∠ZPY = m∠XPW
if m∠WPY = 180 and m∠XPZ = 180, then m∠ZPY = m∠WPX
if m∠WPY = 180 and m∠XPZ = 180, then m∠YPX = m∠WPZ
if m∠WSX = 180 and m∠YSZ = 180 and ray SX bisects ∠TSZ, then m∠WSY = m∠TSX
if m∠XYZ = 180 and ∠PYZ is a right angle, then m∠XYP = 90
if the following are true:
- there is a computer at location x: x y: y z: z and time: t
- z = a + b
then there is a computer at location x: x y: y z: (a + b) and time: t
if the following are true:
- instruction #i is
addi dst=dst src=0 imm=imm - the PC at time t = i
then value of cell dst at time (t + 1) = imm
result of storing 16 at key: c in map: [ ] = [ pair (c, 16), [ ] ]
if the following are true:
- the line at time 0 = 1
- the tab at time 0 = 0
- statement at line 1, tab 0 =
c = 16 - 16 is constant
- Variables Map at time 0 = [ ]
then Variables Map at time 1 = [ entry c: 16, [ ] ]
if the following are true:
- the line at time 0 = 1
- the tab at time 0 = 0
- statement at line 1, tab 0 =
c = 16 - 16 is constant
then the line at time 1 = 2
if the following are true:
- the line at time 0 = 1
- the tab at time 0 = 0
- statement at line 1, tab 0 =
c = 16 - 16 is constant
then the tab at time 1 = 0
if the following are true:
- the line at time 0 = 1
- the tab at time 0 = 0
- statement at line 1, tab 0 =
c = 16 - 16 is constant
then expression state at time 1 = "not_expr"