CubicPathwidth.Alg.Proofs.C1Perm

Source file CubicPathwidth/Alg/Proofs/C1Perm.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Spec

namespace CubicPathwidth.Alg

theorem plainOrderPerm : PlainOrderPerm := by
  intro G Y
  unfold plainOrder
  exact List.mergeSort_perm _ _

theorem switchedOrderPerm : SwitchedOrderPerm := by
  intro G Y
  unfold switchedOrder
  exact List.mergeSort_perm _ _

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.plainOrderPerm
#print axioms CubicPathwidth.Alg.switchedOrderPerm
Back to top