This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| px | ⊦ px(user, p, st) ↔ (∀ q. q ⊑ p → px(user, meta(q, st))) | An Axiom |
| pr | ⊦ pr(user, p, st) ↔ pr(user, meta(p, st)) ∧ (p ≠ ε → px(user, parent(p), st)) | An Axiom |
| pw | ⊦ pw(user, p, st) ↔ pw(user, meta(p, st)) ∧ (p ≠ ε → px(user, parent(p), st)) | An Axiom |
| py | ⊦ py(user, p, st) ↔ pw(user, meta(p, st)) ∧ px(user, p, st) | An Axiom |
| px-app | ⊦ px(user, p + q, st) → (¬ px(user, p, st) ↔ false) | A User Theorem |
| px-eps | ⊦ px(user, ε, st) ↔ px(user, meta(ε, st)) | A User Theorem |
| px-prefix | ⊦ px(user, p, st) ∧ q ⊑ p → (¬ px(user, q, st) ↔ false) | A User Theorem |
| px-to-eps | ⊦ px(user, p, st) → px(user, meta(ε, st)) | A User Theorem |
| py-pw | ⊦ py(user, p, st) → (¬ pw(user, meta(p, st)) ↔ false) | A User Theorem |
| py-px | ⊦ py(user, p, st) → (¬ px(user, p, st) ↔ false) | A User Theorem |