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: |
|---|---|---|
| copy-node | An Axiom | |
| copy-edges | An Axiom | |
| copy-node-prepost | ⊦ copy-node-prepost(H0, H, map) ↔ (∃ H1. H0 ∪ H1 = H ∧ H0 ⊥ H1 ∧ dom map ⊆ dom H0 ∧ ran map = dom H1 ∧ closed(H0) ∧ closed(H1) ∧ inj(map)) | An Axiom |
| copy-edges-prepost | ⊦ copy-edges-prepost(succ, H0, H, map) ↔ (∃ H1. H0 ∪ H1 = H ∧ H0 ⊥ H1 ∧ dom map ⊆ dom H0 ∧ ran map = dom H1 ∧ closed(succ, H1) ∧ closed(H0) ∧ closed(H1) ∧ inj(map)) | An Axiom |
| copy-01 | An Axiom | |
| recursive-property | ⊦ recursive-property(φn, φe) ↔ (∀ n. recursive-node-property(n, φn) ∧ recursive-edges-property(n, φe)) | An Axiom |
| recursive-edges-property | ⊦ recursive-edges-property(n, φe) ↔ (∀ succ0, succ1, H1, map1. [H0 := H1; map0 := map1; copy_edges#(succ0; succ1, map1, H1): n ] φe(succ0, succ1, H0, H1, map0, map1)) | An Axiom |
| recursive-node-property | ⊦ recursive-node-property(n, φn) ↔ (∀ r0, r1, H1, map1. [H0 := H1; map0 := map1; copy_node#(r0; r1, map1, H1): n ] φn(r0, r1, H0, H1, map0, map1)) | An Axiom |
| copy-all-reachable-are-fresh | r0 ∈ H, closed(H), H0 = H ⊦ [copy#(r0; r1, H)] ∀ r2. reachable(r1, r2, H) → ¬ r2 ∈ H0 ∧ r2 ∈ H | A User Theorem |
| copy-edges-empty-term | H0 = H, map0 = map ⊦ ⟪copy_edges#(∅; succ1, map, H)⟫ (H0 = H ∧ map0 = map ∧ succ1 = ∅) | A User Theorem |
| copy-edges-nonempty-term | H1 = H, map1 = map, closed(succ0, H0), copy-edges-prepost(succ1, H0, H, map), ∀ r0, r1, map0, H. map ⊆ map0 ∧ copy-node-prepost(H0, H, map0) ∧ ¬ r0 ∈ map0 ∧ r0 ∈ H0 → ⟪map1 := map0, H1 := H; copy_node#(r0; r1, map0, H)⟫ (copy-node-prepost(H0, H, map0) ∧ H1 ⊆ H ∧ map1 ⊆ map0 ∧ r0 ∈ map0 ∧ map0[r0] = r1) ⊦ ⟪copy_edges#(succ0; succ1, map, H)⟫ (closed(succ0, H0) ∧ H1 ⊆ H ∧ map1 ⊆ map ∧ copy-edges-prepost(succ1, H0, H, map)) | A User Theorem |
| copy-map | ⊦ recursive-property (λ r0, r1, H0, H1, map0, map1. r0 ∈ map1 ∧ map1[r0] = r1, λ succ0, succ1, H0, H1, map0, map1. succ1 = apply(succ0, map1)) | A User Theorem |
| copy-monotone | ⊦ recursive-property (λ r0, r1, H0, H1, map0, map1. H0 ⊆ H1 ∧ map0 ⊆ map1, λ succ0, succ1, H0, H1, map0, map1. H0 ⊆ H1 ∧ map0 ⊆ map1) | A User Theorem |
| copy-new-node | r0 ∈ H0, ¬ r0 ∈ map, H1 = H, map1 = map, copy-node-prepost(H0, H, map) ⊦ ⟪copy_node#(r0; r1, map, H)⟫ (copy-node-prepost(H0, H, map) ∧ H1 ⊆ H ∧ map1 ⊆ map ∧ r0 ∈ map ∧ map[r0] = r1) | A User Theorem |
| copy-no-effects | r0 ∈ H, closed(H), H0 = H ⊦ ⟪copy#(r0; r1, H)⟫ (H0 ⊆ H) | A User Theorem |
| copy-node-prepost-empty | ⊦ closed(H) → (¬ copy-node-prepost(H, H, ∅) ↔ false) | A User Theorem |
| copy-prepost-init | ⊦ copy-node-prepost(H0, H, map) → (¬ copy-edges-prepost(∅, H0, H, map) ↔ false) | A User Theorem |
| copy-prepost-propagate | ⊦ copy-edges-prepost(succ, H0, H, map) → (¬ copy-node-prepost(H0, H, map) ↔ false) | A User Theorem |
| copy-some-edges | ⊦ recursive-edges-property(n, φe) ↔ recursive-edges-property(n, φe) ∧ [H0 := H1; map0 := map1; copy_edges#(succ0; succ1, map1, H1): n ] φe(succ0, succ1, H0, H1, map0, map1) | A User Theorem |
| copy-some-node | ⊦ recursive-node-property(n, φn) ↔ recursive-node-property(n, φn) ∧ [H0 := H1; map0 := map1; copy_node#(r0; r1, map1, H1): n ] φn(r0, r1, H0, H1, map0, map1) | A User Theorem |
| copy-term | r0 ∈ H, closed(H) ⊦ ⟪copy#(r0; r1, H)⟫ true | A User Theorem |
| copy-visited-node | H0 = H, map0 = map, r0 ∈ map ⊦ ⟪copy_node#(r0; r1, map, H)⟫ (H0 = H ∧ map0 = map ∧ r0 ∈ map ∧ r1 = map[r0]) | A User Theorem |
| in-propagate | ⊦ copy-node-prepost(H0, H, map) ∧ r ∈ H0 → (¬ r ∈ H ↔ false) | A User Theorem |
| prove-recursion | ∀ m. (∀ n. n < m → recursive-node-property(n, φn) ∧ recursive-edges-property(n, φe)) → (∀ r0, r1, H1, map1. [H0 := H1; map0 := map1; copy_node#(r0; r1, map1, H1): m ] φn(r0, r1, H0, H1, map0, map1)) ∧ (∀ succ0, succ1, H1, map1. [H0 := H1; map0 := map1; copy_edges#(succ0; succ1, map1, H1): m ] φe(succ0, succ1, H0, H1, map0, map1)) ⊦ recursive-property(φn, φe) | A User Theorem |
| smaller | ⊦ copy-node-prepost(H0, H, map) → # map ≤ # H0 | A User Theorem |
| strengthen-recursive-edges-property | ⊦ recursive-property(φn0, φe0) → ( ¬ ¬ recursive-edges-property(n, φe1) ↔ recursive-edges-property (n, λ succ0, succ1, H0, H1, map0, map1. φe0(succ0, succ1, H0, H1, map0, map1) ∧ φe1(succ0, succ1, H0, H1, map0, map1))) | A User Theorem |
| strengthen-recursive-node-property | ⊦ recursive-property(φn0, φe0) → ( ¬ ¬ recursive-node-property(n, φn1) ↔ recursive-node-property(n, λ r0, r1, H0, H1, map0, map1. φn0(r0, r1, H0, H1, map0, map1) ∧ φn1(r0, r1, H0, H1, map0, map1))) | A User Theorem |
| subset-eq | ⊦ H ⊆ H | A User Theorem |
| subset-smaller | ⊦ map0 ⊆ map1 → # map0 ≤ # map1 | A User Theorem |
| subset-trans | ⊦ H0 ⊆ H1 ∧ H1 ⊆ H2 → H0 ⊆ H2 | A User Theorem |