Function disjoint_domains 

pub open spec fn disjoint_domains<P1: SpecParser, P2: SpecParser>(p1: P1, p2: P2) -> bool

{
    forall |input: Seq<u8>| (
        p1.spec_parse(input) is Some && p2.spec_parse(input) is Some ==> false
    )
}

Two parsers have disjoint domains if no input can be successfully parsed by both.

This is the key condition for establishing unambiguity in combinator compositions. See also crate::combinators::disjoint for broadcast lemmas establishing disjointness for common compositions.