Module prop::qubit

Path Semantical Qubit

For an implementation, see the Pocket-Prover library.

Structs

• Qubit
  Represents a recursive qubit proposition.

Functions

• decide
  ~a ⋁ ¬~a.
• decide_tauto_excm
  (a ⋁ ¬a)^true => (~a ⋁ ¬~a).
• eq_q_qu
  (a ~~ a) == ~a.
• eq_qu_q
  ~a == (a ~~ a).
• eq_sesh_inv
  ¬~a == ~¬a.
• eq_to_eq_inv
  (~a == ~b) => (~¬a == ~¬b).`
• from_eq
  Convert from equality.
• from_eq_q
  Convert from equality.
• in_arg
  ~a ∧ (a == b)^true => ~b.
• inv_to_sesh
  ~¬a => ¬~a.
• normalize
  ~qubit^n(a) => qubit^(n+1)(a).
• rev_normalize
  qubit^(n+1)(a) => ~qubit^n(a).
• sesh_to_inv
  ¬~a => ~¬a.
• to_eq
  Convert to equality.
• to_eq_q
  Convert to equality.

Type Definitions

• Qu
  The qubit proposition ~a.