Orientation symmetry of the actual Pauli decision program

def MIPRE.QLD.PauliBooleanProgram.swapInput (input : Input) : Input

Equations

• MIPRE.QLD.PauliBooleanProgram.swapInput input = (input.1, input.2.2, input.2.1)

theorem MIPRE.QLD.PauliBooleanProgram.route_kind_symm (T U : Ty) : (PauliBranchProgram.route U T).1 = (PauliBranchProgram.route T U).1

theorem MIPRE.QLD.PauliBooleanProgram.route_metadata_symm (T U : Ty) : (PauliBranchProgram.route U T).2.2 = (PauliBranchProgram.route T U).2.2

theorem MIPRE.QLD.PauliBooleanProgram.route_flip (T U : Ty) (h0 : 0 < (PauliBranchProgram.route T U).1) (h8 : (PauliBranchProgram.route T U).1 < 8) : (PauliBranchProgram.route U T).2.1 = !(PauliBranchProgram.route T U).2.1

theorem MIPRE.QLD.PauliBooleanProgram.route_kind_swap (input : Input) : (route.toFun (swapInput input)).1 = (route.toFun input).1

theorem MIPRE.QLD.PauliBooleanProgram.basis_swap (input : Input) : basis.toFun (swapInput input) = basis.toFun input

theorem MIPRE.QLD.PauliBooleanProgram.oriented_swap (input : Input) (h0 : 0 < (route.toFun input).1) (h8 : (route.toFun input).1 < 8) : oriented.toFun (swapInput input) = oriented.toFun input

theorem MIPRE.QLD.PauliBooleanProgram.checks_swap (input : Input) (h0 : 0 < (route.toFun input).1) (h8 : (route.toFun input).1 < 8) : checks.toFun (swapInput input) = checks.toFun input

theorem MIPRE.QLD.PauliBooleanProgram.parsers_swap (input : Input) (h0 : 0 < (route.toFun input).1) (h8 : (route.toFun input).1 < 8) : leftParser.toFun (swapInput input) = leftParser.toFun input ∧ rightParser.toFun (swapInput input) = rightParser.toFun input

theorem MIPRE.QLD.PauliBooleanProgram.program_swap_handled (input : Input) (h0 : 0 < (route.toFun input).1) (h8 : (route.toFun input).1 < 8) : program.toFun (swapInput input) = program.toFun input

def MIPRE.QLD.PauliBooleanProgram.Forward (T U : Ty) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.QLD.PauliBooleanProgram.forward_or_reverse (T U : Ty) (h0 : 0 < (PauliBranchProgram.route T U).1) (h8 : (PauliBranchProgram.route T U).1 < 8) : Forward T U ∨ Forward U T

theorem MIPRE.QLD.PauliBooleanProgram.route_default_unhandled (T U : Ty) (h : (PauliBranchProgram.route T U).1 = 8) : handled T U = false