Axiom ax-newstateeq 1045

Description: This is the simplest known example of an equation implied by the set of Mayet--Godowski equations that is independent from all Godowski equations. It was discovered by Norman Megill and Mladen Pavicic between 1997 and August 2003. This is Equation (54) in

Mladen Pavicic, Norman D. Megill, Quantum Logic and Quantum Computation, in Handbook of Quantum Logic and Quantum Structures, Volume Quantum Structures, Elsevier, Amsterdam, 2007, pp. 751--787. https://arxiv.org/abs/0812.3072

and Equation (15) in

Mladen Pavicic, Brendan D. McKay, Norman D. Megill, Kresimir Fresl, Graph Approach to Quantum Systems, Journal of Mathematical Physics, Volume 51, Issue 10, October 2010. https://arxiv.org/abs/1004.0776

(Contributed by NM, 1-Jan-1998.)

Assertion

Ref	Expression
ax-newstateeq	(((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a)

Detailed syntax breakdown of Axiom ax-newstateeq

Step	Hyp	Ref	Expression
1		wva	. . . . 5 term  a
2		wvb	. . . . 5 term  b
3	1, 2	wi1 12	. . . 4 term  (a →1 b)
4		wvc	. . . . 5 term  c
5	4, 2	wi1 12	. . . 4 term  (c →1 b)
6	3, 5	wi1 12	. . 3 term  ((a →1 b) →1 (c →1 b))
7	1, 4	wi1 12	. . . 4 term  (a →1 c)
8	2, 1	wi1 12	. . . 4 term  (b →1 a)
9	7, 8	wa 7	. . 3 term  ((a →1 c) ∩ (b →1 a))
10	6, 9	wa 7	. 2 term  (((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a)))
11	4, 1	wi1 12	. 2 term  (c →1 a)
12	10, 11	wle 2	1 wff  (((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a)

This axiom is referenced by: (None)