(no title)
litexlang | 5 months ago
Since transitivity of >= is not implemented, one has to call this self_defined_axiom_larger_equal_is_transitive to make x >= 17 here, so
``` know forall x N: x >= 47 => x >= 17 ```
is essential
litexlang | 5 months ago
Since transitivity of >= is not implemented, one has to call this self_defined_axiom_larger_equal_is_transitive to make x >= 17 here, so
``` know forall x N: x >= 47 => x >= 17 ```
is essential
No comments yet.