|
|
|
|
|
|
by litexlang
264 days ago
|
|
|
know @self_defined_axiom_larger_equal_is_transitive(x, y, z R):
x >= y
y >= z
=>:
x >= z 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 |
|
|