We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 024ddd6 commit 33c626eCopy full SHA for 33c626e
docs/2020-06-30-Combining-Priority-Axioms.md
@@ -74,16 +74,19 @@ priority rewrite rule.
74
...
75
∧ ¬ (∃ Xn . ⌈ β(X₁) ∧ φn(Xn) ∧ Pn(Xn) ⌉)
76
⌉
77
+ ∧ ⌈β(X₁)∧ φ(X)⌉ ∧ P(X)
78
// If P is a predicate then ⌈φ∧P⌉=⌈φ⌉∧P
79
= ⌈β(X₁)
80
∧ ¬ (∃ X₁ . ⌈ β(X₁) ∧ φ₁(X₁) ⌉ ∧ P₁(X₁))
81
82
∧ ¬ (∃ Xn . ⌈ β(X₁) ∧ φn(Xn) ⌉ ∧ Pn(Xn))
83
84
85
// If P is a predicate then ∃ X . P is a predicate
86
87
= ⌈β(X₁)⌉
- ∧ ¬ (∃ X₁ . ⌈ β(X₁) ∧ φ₁(X₁) ⌉ ∧ P₁(X₁))
- ...
88
- ∧ ¬ (∃ Xn . ⌈ β(X₁) ∧ φn(Xn) ⌉ ∧ Pn(Xn))
+ ∧ ¬ (∃ X₁ . ⌈ β(X₁) ∧ φ₁(X₁) ⌉ ∧ P₁(X₁))
89
+ ...
90
+ ∧ ¬ (∃ Xn . ⌈ β(X₁) ∧ φn(Xn) ⌉ ∧ Pn(Xn))
91
92
```
0 commit comments