QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-newstateeq Unicode version
Axiom ax-newstateeq 1045
Description: New equation that holds in Hilbert space, discovered by Pavicic and Megill (unpublished).
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
StepHypRef Expression
1 wva . . . . 5 term a
2 wvb . . . . 5 term b
31, 2wi1 12 . . . 4 term (a ->1 b)
4 wvc . . . . 5 term c
54, 2wi1 12 . . . 4 term (c ->1 b)
63, 5wi1 12 . . 3 term ((a ->1 b) ->1 (c ->1 b))
71, 4wi1 12 . . . 4 term (a ->1 c)
82, 1wi1 12 . . . 4 term (b ->1 a)
97, 8wa 7 . . 3 term ((a ->1 c) ^ (b ->1 a))
106, 9wa 7 . 2 term (((a ->1 b) ->1 (c ->1 b)) ^ ((a ->1 c) ^ (b ->1 a)))
114, 1wi1 12 . 2 term (c ->1 a)
1210, 11wle 2 1 wff (((a ->1 b) ->1 (c ->1 b)) ^ ((a ->1 c) ^ (b ->1 a))) =< (c ->1 a)
Colors of variables: term
This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator