Fin 4 cancellation: 88 chamber proofs

Each chamber corresponds to a weight vector (w0, w1, w2, w3) with w0 >= w1 >= w2 >= w3 determining which subset-comparison hypotheses hold. solve_cancellation derives all needed ge/nge facts from the weights and applies cancellation_from_pairs.

theorem Core.Scale.chamber_0 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : ¬sys.ge {2, 3} {1}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_1 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : ¬sys.ge {2, 3} {1}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_2 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_3 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_4 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_5 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_6 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : sys.ge {2, 3} {1}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_7 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : sys.ge {2, 3} {1}) (hf6r : ¬sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_8 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : ¬sys.ge {1, 2} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_9 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_10 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : ¬sys.ge {2, 3} {1}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_11 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : ¬sys.ge {2, 3} {1}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_12 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_13 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : sys.ge {1, 2} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_14 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_15 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_16 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_17 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_18 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_19 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_20 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_21 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_22 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_23 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_24 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_25 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : ¬sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_26 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : ¬sys.ge {1, 2} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_27 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : ¬sys.ge {1, 2} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_28 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : ¬sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_29 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_30 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : ¬sys.ge {1, 2} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_31 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_32 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_33 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_34 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_35 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_36 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : sys.ge {2, 3} {1}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_37 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : sys.ge {0} {1, 2, 3}) (hf5r : sys.ge {2, 3} {1}) (hf6r : sys.ge {1, 2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_38 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf3r : ¬sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_39 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_40 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : sys.ge {1, 2} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_41 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : sys.ge {1, 2} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_42 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_43 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf4r : sys.ge {1, 2} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_44 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : ¬sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_45 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_46 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf3r : ¬sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_47 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_48 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_49 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf3r : ¬sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_50 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_51 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_52 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf3r : sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_53 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_54 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_55 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_56 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_57 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_58 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_59 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf2r : ¬sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_60 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_61 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf3r : sys.ge {1, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_62 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_63 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_64 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_65 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf3r : sys.ge {1, 3} {0}) (hf5r : sys.ge {2, 3} {1}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_66 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_67 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_68 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_69 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_70 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_71 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_72 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : ¬sys.ge {1, 2} {0, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_73 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_74 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_75 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_76 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_77 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_78 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_79 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_80 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_81 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : ¬sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_82 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_83 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_84 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_85 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : ¬sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf1r : sys.ge {1, 2} {0, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_86 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) (hf1 : ¬sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge

theorem Core.Scale.chamber_87 (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) (hf1 : sys.ge {0, 3} {1, 2}) (hf2 : sys.ge {0} {2, 3}) (hf3 : ¬sys.ge {0} {1, 3}) (hf4 : ¬sys.ge {0} {1, 2}) (hf5 : sys.ge {1} {2, 3}) (hf6 : ¬sys.ge {0} {1, 2, 3}) (hf2r : sys.ge {2, 3} {0}) : Cancellation 4 sys.ge