Test biconditionals

This commit is contained in:
Patrick Lühne 2020-04-07 17:50:00 +02:00
parent 0c132edc07
commit 21d4b1d605
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF

View File

@ -1756,6 +1756,67 @@ mod tests
if_and_only_if(vec![implies_left(p2(), q2())]))),
"q2 <- p2 <- (q1 <- p1)");
// TODO: Implies + if and only if
// Implies + if and only if
assert_eq!(format(
implies_right(if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()))),
"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
assert_eq!(format(
implies_right(and(vec![if_and_only_if(p1q1r1())]),
and(vec![if_and_only_if(p2q2r2())]))),
"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
assert_eq!(format(
implies_right(or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]))),
"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
assert_eq!(format(
implies_right(if_and_only_if(vec![if_and_only_if(p1q1r1())]),
if_and_only_if(vec![if_and_only_if(p2q2r2())]))),
"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
assert_eq!(format(
implies_left(if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()))),
"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
assert_eq!(format(
implies_left(and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]))),
"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
assert_eq!(format(
implies_left(or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]))),
"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
assert_eq!(format(
implies_left(if_and_only_if(vec![if_and_only_if(p1q1r1())]),
if_and_only_if(vec![if_and_only_if(p2q2r2())]))),
"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
assert_eq!(format(
if_and_only_if(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
implies_right(p3(), q3())])),
"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
assert_eq!(format(
if_and_only_if(vec![and(vec![implies_right(p1(), q1())]),
and(vec![implies_right(p2(), q2())]), and(vec![implies_right(p3(), q3())])])),
"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
assert_eq!(format(
if_and_only_if(vec![or(vec![implies_right(p1(), q1())]),
or(vec![implies_right(p2(), q2())]), or(vec![implies_right(p3(), q3())])])),
"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
assert_eq!(format(
if_and_only_if(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
if_and_only_if(vec![implies_right(p2(), q2())]),
if_and_only_if(vec![implies_right(p3(), q3())])])),
"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
assert_eq!(format(
if_and_only_if(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
implies_left(p3(), q3())])),
"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
assert_eq!(format(
if_and_only_if(vec![and(vec![implies_left(p1(), q1())]),
and(vec![implies_left(p2(), q2())]), and(vec![implies_left(p3(), q3())])])),
"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
assert_eq!(format(
if_and_only_if(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
or(vec![implies_left(p3(), q3())])])),
"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
assert_eq!(format(
if_and_only_if(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
if_and_only_if(vec![implies_left(p2(), q2())]),
if_and_only_if(vec![implies_left(p3(), q3())])])),
"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
}
}