kdrag.property.Trans

kdrag.property.Trans(rel) → BoolRef

>>> Trans(smt.Function("rel", smt.IntSort(), smt.IntSort(), smt.BoolSort()))
ForAll([x, y, z], Implies(And(rel(x, y), rel(y, z)), rel(x, z)))