Function prop::path_semantics::assume_norm_path_level [−][src]
pub fn assume_norm_path_level<A: LProp, B: LProp, C: LProp, D: LProp>(
) -> PSemNaiveNorm<A, B, C, D> where
(A::N, B::N): SortMin<A, B> + SortMax<A, B>,
(C::N, D::N): SortMin<C, D> + SortMax<C, D>,
(<Min<A, B> as LProp>::N, <Min<C, D> as LProp>::N): SortMin<Min<A, B>, Min<C, D>> + SortMax<Min<A, B>, Min<C, D>>,
(<Max<A, B> as LProp>::N, <Max<C, D> as LProp>::N): SortMin<Max<A, B>, Max<C, D>> + SortMax<Max<A, B>, Max<C, D>>,
(<MaxMin<A, B, C, D> as LProp>::N, <MinMax<A, B, C, D> as LProp>::N): SortMin<MaxMin<A, B, C, D>, MinMax<A, B, C, D>> + SortMax<MaxMin<A, B, C, D>, MinMax<A, B, C, D>>,
<MinMin<A, B, C, D> as LProp>::N: Lt<<Maxi<A, B, C, D> as LProp>::N>,
Assume a normalised naive core axiom.
The orientation is detected automatically and restored to a naive core axiom which has a proof to any valid order.