Documentation

Linglib.Core.Scales.EpistemicScale.CancellationHelpers

Shared helpers for Fin 4 cancellation chamber proofs #

Auto-generated helper lemmas used by the 88 chamber proofs.

theorem Core.Scale.sd_0_0 :

{0} \ {0} = ∅

theorem Core.Scale.sd_0_01 :

{0} \ {0, 1} = ∅

theorem Core.Scale.sd_0_02 :

{0} \ {0, 2} = ∅

theorem Core.Scale.sd_0_03 :

{0} \ {0, 3} = ∅

theorem Core.Scale.sd_0_012 :

{0} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_0_013 :

{0} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_0_023 :

{0} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_0_0123 :

{0} \ Set.univ = ∅

theorem Core.Scale.sd_1_1 :

{1} \ {1} = ∅

theorem Core.Scale.sd_1_01 :

{1} \ {0, 1} = ∅

theorem Core.Scale.sd_1_12 :

{1} \ {1, 2} = ∅

theorem Core.Scale.sd_1_13 :

{1} \ {1, 3} = ∅

theorem Core.Scale.sd_1_012 :

{1} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_1_013 :

{1} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_1_123 :

{1} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_1_0123 :

{1} \ Set.univ = ∅

theorem Core.Scale.sd_2_2 :

{2} \ {2} = ∅

theorem Core.Scale.sd_2_02 :

{2} \ {0, 2} = ∅

theorem Core.Scale.sd_2_12 :

{2} \ {1, 2} = ∅

theorem Core.Scale.sd_2_23 :

{2} \ {2, 3} = ∅

theorem Core.Scale.sd_2_012 :

{2} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_2_023 :

{2} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_2_123 :

{2} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_2_0123 :

{2} \ Set.univ = ∅

theorem Core.Scale.sd_3_3 :

{3} \ {3} = ∅

theorem Core.Scale.sd_3_03 :

{3} \ {0, 3} = ∅

theorem Core.Scale.sd_3_13 :

{3} \ {1, 3} = ∅

theorem Core.Scale.sd_3_23 :

{3} \ {2, 3} = ∅

theorem Core.Scale.sd_3_013 :

{3} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_3_023 :

{3} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_3_123 :

{3} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_3_0123 :

{3} \ Set.univ = ∅

theorem Core.Scale.sd_01_0 :

{0, 1} \ {0} = {1}

theorem Core.Scale.sd_01_1 :

{0, 1} \ {1} = {0}

theorem Core.Scale.sd_01_01 :

{0, 1} \ {0, 1} = ∅

theorem Core.Scale.sd_01_02 :

{0, 1} \ {0, 2} = {1}

theorem Core.Scale.sd_01_03 :

{0, 1} \ {0, 3} = {1}

theorem Core.Scale.sd_01_12 :

{0, 1} \ {1, 2} = {0}

theorem Core.Scale.sd_01_13 :

{0, 1} \ {1, 3} = {0}

theorem Core.Scale.sd_01_012 :

{0, 1} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_01_013 :

{0, 1} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_01_023 :

{0, 1} \ {0, 2, 3} = {1}

theorem Core.Scale.sd_01_123 :

{0, 1} \ {1, 2, 3} = {0}

theorem Core.Scale.sd_01_0123 :

{0, 1} \ Set.univ = ∅

theorem Core.Scale.sd_02_0 :

{0, 2} \ {0} = {2}

theorem Core.Scale.sd_02_2 :

{0, 2} \ {2} = {0}

theorem Core.Scale.sd_02_01 :

{0, 2} \ {0, 1} = {2}

theorem Core.Scale.sd_02_02 :

{0, 2} \ {0, 2} = ∅

theorem Core.Scale.sd_02_03 :

{0, 2} \ {0, 3} = {2}

theorem Core.Scale.sd_02_12 :

{0, 2} \ {1, 2} = {0}

theorem Core.Scale.sd_02_23 :

{0, 2} \ {2, 3} = {0}

theorem Core.Scale.sd_02_012 :

{0, 2} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_02_013 :

{0, 2} \ {0, 1, 3} = {2}

theorem Core.Scale.sd_02_023 :

{0, 2} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_02_123 :

{0, 2} \ {1, 2, 3} = {0}

theorem Core.Scale.sd_02_0123 :

{0, 2} \ Set.univ = ∅

theorem Core.Scale.sd_03_0 :

{0, 3} \ {0} = {3}

theorem Core.Scale.sd_03_3 :

{0, 3} \ {3} = {0}

theorem Core.Scale.sd_03_01 :

{0, 3} \ {0, 1} = {3}

theorem Core.Scale.sd_03_02 :

{0, 3} \ {0, 2} = {3}

theorem Core.Scale.sd_03_03 :

{0, 3} \ {0, 3} = ∅

theorem Core.Scale.sd_03_13 :

{0, 3} \ {1, 3} = {0}

theorem Core.Scale.sd_03_23 :

{0, 3} \ {2, 3} = {0}

theorem Core.Scale.sd_03_012 :

{0, 3} \ {0, 1, 2} = {3}

theorem Core.Scale.sd_03_013 :

{0, 3} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_03_023 :

{0, 3} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_03_123 :

{0, 3} \ {1, 2, 3} = {0}

theorem Core.Scale.sd_03_0123 :

{0, 3} \ Set.univ = ∅

theorem Core.Scale.sd_12_1 :

{1, 2} \ {1} = {2}

theorem Core.Scale.sd_12_2 :

{1, 2} \ {2} = {1}

theorem Core.Scale.sd_12_01 :

{1, 2} \ {0, 1} = {2}

theorem Core.Scale.sd_12_02 :

{1, 2} \ {0, 2} = {1}

theorem Core.Scale.sd_12_12 :

{1, 2} \ {1, 2} = ∅

theorem Core.Scale.sd_12_13 :

{1, 2} \ {1, 3} = {2}

theorem Core.Scale.sd_12_23 :

{1, 2} \ {2, 3} = {1}

theorem Core.Scale.sd_12_012 :

{1, 2} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_12_013 :

{1, 2} \ {0, 1, 3} = {2}

theorem Core.Scale.sd_12_023 :

{1, 2} \ {0, 2, 3} = {1}

theorem Core.Scale.sd_12_123 :

{1, 2} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_12_0123 :

{1, 2} \ Set.univ = ∅

theorem Core.Scale.sd_13_1 :

{1, 3} \ {1} = {3}

theorem Core.Scale.sd_13_3 :

{1, 3} \ {3} = {1}

theorem Core.Scale.sd_13_01 :

{1, 3} \ {0, 1} = {3}

theorem Core.Scale.sd_13_03 :

{1, 3} \ {0, 3} = {1}

theorem Core.Scale.sd_13_12 :

{1, 3} \ {1, 2} = {3}

theorem Core.Scale.sd_13_13 :

{1, 3} \ {1, 3} = ∅

theorem Core.Scale.sd_13_23 :

{1, 3} \ {2, 3} = {1}

theorem Core.Scale.sd_13_012 :

{1, 3} \ {0, 1, 2} = {3}

theorem Core.Scale.sd_13_013 :

{1, 3} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_13_023 :

{1, 3} \ {0, 2, 3} = {1}

theorem Core.Scale.sd_13_123 :

{1, 3} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_13_0123 :

{1, 3} \ Set.univ = ∅

theorem Core.Scale.sd_23_2 :

{2, 3} \ {2} = {3}

theorem Core.Scale.sd_23_3 :

{2, 3} \ {3} = {2}

theorem Core.Scale.sd_23_02 :

{2, 3} \ {0, 2} = {3}

theorem Core.Scale.sd_23_03 :

{2, 3} \ {0, 3} = {2}

theorem Core.Scale.sd_23_12 :

{2, 3} \ {1, 2} = {3}

theorem Core.Scale.sd_23_13 :

{2, 3} \ {1, 3} = {2}

theorem Core.Scale.sd_23_23 :

{2, 3} \ {2, 3} = ∅

theorem Core.Scale.sd_23_012 :

{2, 3} \ {0, 1, 2} = {3}

theorem Core.Scale.sd_23_013 :

{2, 3} \ {0, 1, 3} = {2}

theorem Core.Scale.sd_23_023 :

{2, 3} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_23_123 :

{2, 3} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_23_0123 :

{2, 3} \ Set.univ = ∅

theorem Core.Scale.sd_012_0 :

{0, 1, 2} \ {0} = {1, 2}

theorem Core.Scale.sd_012_1 :

{0, 1, 2} \ {1} = {0, 2}

theorem Core.Scale.sd_012_2 :

{0, 1, 2} \ {2} = {0, 1}

theorem Core.Scale.sd_012_01 :

{0, 1, 2} \ {0, 1} = {2}

theorem Core.Scale.sd_012_02 :

{0, 1, 2} \ {0, 2} = {1}

theorem Core.Scale.sd_012_03 :

{0, 1, 2} \ {0, 3} = {1, 2}

theorem Core.Scale.sd_012_12 :

{0, 1, 2} \ {1, 2} = {0}

theorem Core.Scale.sd_012_13 :

{0, 1, 2} \ {1, 3} = {0, 2}

theorem Core.Scale.sd_012_23 :

{0, 1, 2} \ {2, 3} = {0, 1}

theorem Core.Scale.sd_012_012 :

{0, 1, 2} \ {0, 1, 2} = ∅

theorem Core.Scale.sd_012_013 :

{0, 1, 2} \ {0, 1, 3} = {2}

theorem Core.Scale.sd_012_023 :

{0, 1, 2} \ {0, 2, 3} = {1}

theorem Core.Scale.sd_012_123 :

{0, 1, 2} \ {1, 2, 3} = {0}

theorem Core.Scale.sd_012_0123 :

{0, 1, 2} \ Set.univ = ∅

theorem Core.Scale.sd_013_0 :

{0, 1, 3} \ {0} = {1, 3}

theorem Core.Scale.sd_013_1 :

{0, 1, 3} \ {1} = {0, 3}

theorem Core.Scale.sd_013_3 :

{0, 1, 3} \ {3} = {0, 1}

theorem Core.Scale.sd_013_01 :

{0, 1, 3} \ {0, 1} = {3}

theorem Core.Scale.sd_013_02 :

{0, 1, 3} \ {0, 2} = {1, 3}

theorem Core.Scale.sd_013_03 :

{0, 1, 3} \ {0, 3} = {1}

theorem Core.Scale.sd_013_12 :

{0, 1, 3} \ {1, 2} = {0, 3}

theorem Core.Scale.sd_013_13 :

{0, 1, 3} \ {1, 3} = {0}

theorem Core.Scale.sd_013_23 :

{0, 1, 3} \ {2, 3} = {0, 1}

theorem Core.Scale.sd_013_012 :

{0, 1, 3} \ {0, 1, 2} = {3}

theorem Core.Scale.sd_013_013 :

{0, 1, 3} \ {0, 1, 3} = ∅

theorem Core.Scale.sd_013_023 :

{0, 1, 3} \ {0, 2, 3} = {1}

theorem Core.Scale.sd_013_123 :

{0, 1, 3} \ {1, 2, 3} = {0}

theorem Core.Scale.sd_013_0123 :

{0, 1, 3} \ Set.univ = ∅

theorem Core.Scale.sd_023_0 :

{0, 2, 3} \ {0} = {2, 3}

theorem Core.Scale.sd_023_2 :

{0, 2, 3} \ {2} = {0, 3}

theorem Core.Scale.sd_023_3 :

{0, 2, 3} \ {3} = {0, 2}

theorem Core.Scale.sd_023_01 :

{0, 2, 3} \ {0, 1} = {2, 3}

theorem Core.Scale.sd_023_02 :

{0, 2, 3} \ {0, 2} = {3}

theorem Core.Scale.sd_023_03 :

{0, 2, 3} \ {0, 3} = {2}

theorem Core.Scale.sd_023_12 :

{0, 2, 3} \ {1, 2} = {0, 3}

theorem Core.Scale.sd_023_13 :

{0, 2, 3} \ {1, 3} = {0, 2}

theorem Core.Scale.sd_023_23 :

{0, 2, 3} \ {2, 3} = {0}

theorem Core.Scale.sd_023_012 :

{0, 2, 3} \ {0, 1, 2} = {3}

theorem Core.Scale.sd_023_013 :

{0, 2, 3} \ {0, 1, 3} = {2}

theorem Core.Scale.sd_023_023 :

{0, 2, 3} \ {0, 2, 3} = ∅

theorem Core.Scale.sd_023_123 :

{0, 2, 3} \ {1, 2, 3} = {0}

theorem Core.Scale.sd_023_0123 :

{0, 2, 3} \ Set.univ = ∅

theorem Core.Scale.sd_123_1 :

{1, 2, 3} \ {1} = {2, 3}

theorem Core.Scale.sd_123_2 :

{1, 2, 3} \ {2} = {1, 3}

theorem Core.Scale.sd_123_3 :

{1, 2, 3} \ {3} = {1, 2}

theorem Core.Scale.sd_123_01 :

{1, 2, 3} \ {0, 1} = {2, 3}

theorem Core.Scale.sd_123_02 :

{1, 2, 3} \ {0, 2} = {1, 3}

theorem Core.Scale.sd_123_03 :

{1, 2, 3} \ {0, 3} = {1, 2}

theorem Core.Scale.sd_123_12 :

{1, 2, 3} \ {1, 2} = {3}

theorem Core.Scale.sd_123_13 :

{1, 2, 3} \ {1, 3} = {2}

theorem Core.Scale.sd_123_23 :

{1, 2, 3} \ {2, 3} = {1}

theorem Core.Scale.sd_123_012 :

{1, 2, 3} \ {0, 1, 2} = {3}

theorem Core.Scale.sd_123_013 :

{1, 2, 3} \ {0, 1, 3} = {2}

theorem Core.Scale.sd_123_023 :

{1, 2, 3} \ {0, 2, 3} = {1}

theorem Core.Scale.sd_123_123 :

{1, 2, 3} \ {1, 2, 3} = ∅

theorem Core.Scale.sd_123_0123 :

{1, 2, 3} \ Set.univ = ∅

theorem Core.Scale.sd_0123_0 :

Set.univ \ {0} = {1, 2, 3}

theorem Core.Scale.sd_0123_1 :

Set.univ \ {1} = {0, 2, 3}

theorem Core.Scale.sd_0123_2 :

Set.univ \ {2} = {0, 1, 3}

theorem Core.Scale.sd_0123_3 :

Set.univ \ {3} = {0, 1, 2}

theorem Core.Scale.sd_0123_01 :

Set.univ \ {0, 1} = {2, 3}

theorem Core.Scale.sd_0123_02 :

Set.univ \ {0, 2} = {1, 3}

theorem Core.Scale.sd_0123_03 :

Set.univ \ {0, 3} = {1, 2}

theorem Core.Scale.sd_0123_12 :

Set.univ \ {1, 2} = {0, 3}

theorem Core.Scale.sd_0123_13 :

Set.univ \ {1, 3} = {0, 2}

theorem Core.Scale.sd_0123_23 :

Set.univ \ {2, 3} = {0, 1}

theorem Core.Scale.sd_0123_012 :

Set.univ \ {0, 1, 2} = {3}

theorem Core.Scale.sd_0123_013 :

Set.univ \ {0, 1, 3} = {2}

theorem Core.Scale.sd_0123_023 :

Set.univ \ {0, 2, 3} = {1}

theorem Core.Scale.sd_0123_123 :

Set.univ \ {1, 2, 3} = {0}

theorem Core.Scale.sd_0123_0123 :

Set.univ \ Set.univ = ∅