quality_core_eq_propagation/
quality_core_eq_propagation.rs

1/*
2
3This example shows that when the strong version of
4the path semantical core axiom is used,
5equality of quality propagates to values of types.
6
7Quality here might be thought of as identification of symbols.
8
9The strong version of the core axiom assumes
10that when types are identified, their values can be identified.
11The weak version of the core axiom only assumes
12that when values are identified, their types can be identified.
13
14*/
15
16use pocket_prover::*;
17
18fn main() {
19    println!("{}", measure(10, || prove!(&mut |a0, b0, a1, b1, c, d| {
20        imply(
21            and(
22                ps_core_eq(a0, b0, c, d),
23                ps_core_eq(a1, b1, c, d),
24            ),
25            imply(
26                and!(
27                    imply(a0, c),
28                    imply(b0, d),
29                    imply(a1, c),
30                    imply(b1, d),
31                ),
32                eq(qual(a0, b0), qual(a1, b1))
33            )
34        )
35    })));
36}