| |
| 2.5 Properties of
chop-plus
Proof:
1 | ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ | |
2 | ⊢ f ⊃ f+ | |
qed
| ⊢ | f ; f+ ⊃ f+ | | ChopChopPlusImpChopPlus |
Proof:
1 | ⊢ empty ∨ more | |
2 | ⊢ f ⊃ empty ∨ (f ∧ more) | |
3 | ⊢ f ; f+ ⊃ f+ ∨ (f ∧ more) ; f+ | |
4 | ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ | |
5 | ⊢ (f ∧ more) ; f+ ⊃ f+ | |
6 | ⊢ f ; f+ ⊃ f+ | |
|
qed
| ⊢ | f+ ≡ f ∨ (f ; f+) | | ChopPlusEqvOrChopChopPlus |
Proof for ⊃:
1 | ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ | |
2 | ⊢ (f ∧ more) ; f+ ⊃ f ; f+ | |
3 | ⊢ f+ ⊃ f ∨ f ; f+ | |
qed
Proof for ⊂:
1 | ⊢ f ⊃ f+ | |
2 | ⊢ empty ∨ more | |
3 | ⊢ f ⊃ empty ∨ (f ∧ more) | |
4 | ⊢ f ; f+ ⊃ f+ ∨ (f ∧ more) ; f+ | |
5 | ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ | |
6 | ⊢ (f ∧ more) ; f+ ⊃ f+ | |
7 | ⊢ f ∨ (f ; f+) ⊃ f+ | |
qed
| ⊢ | f ∧¬g ⊃ (g ∧ more) ; f ⇒ ⊢ f ⊃ g+ | | ChopPlusIntro |
Proof:
1 | ⊢ f ∧¬g ⊃ (g ∧ more) ; f | given |
2 | ⊢ g+ ≡ g ∨ (g ∧ more) ; g+ | |
3 | ⊢ f ∧¬(g+) ⊃ (g ∧ more) ; f ∧¬((g ∧ more) ; g+) | |
4 | ⊢ g ∧ more ⊃ more | |
5 | ⊢ f ⊃ g+ | |
qed
| ⊢ | f ⊃g, ⊢ (f ∧ more) ; g ⊃g ⇒ ⊢ f+ ⊃g | | ChopPlusElim |
Proof:
1 | ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ | |
2 | ⊢ f ⊃g | given |
3 | ⊢ (f ∧ more) ; g ⊃g | given |
4 | ⊢ f+ ∧¬g ⊃ (f ∧ more) ; f+ ∧¬((f ∧ more) ; g) | |
5 | ⊢ f ∧ more ⊃ more | |
6 | ⊢ f+ ⊃ g | |
qed
| ⊢ | f ⊃g, ⊢ f ; g ⊃g ⇒ ⊢ f+ ⊃g | | ChopPlusElimWithoutMore |
Proof:
1 | ⊢ f ⊃ g | given |
2 | ⊢ f ; g ⊃ g | given |
3 | ⊢ (f ∧ more) ; g ⊃ f ; g | |
4 | ⊢ (f ∧ more) ; g ⊃ g | |
5 | ⊢ f+ ⊃ g | |
qed
| ⊢ | f ⊃g ⇒ ⊢ f+ ⊃g+ | | ChopPlusImpChopPlus |
Proof:
1 | ⊢ f ⊃ g | given |
2 | ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ | |
3 | ⊢ g+ ≡ g ∨ (g ∧ more) ; g+ | |
4 | ⊢ f+ ∧¬(g+) ⊃ ((f ∧ more) ; f+) ∧¬((g ∧ more) ; g+) | |
5 | ⊢ f ∧ more ⊃ g ∧ more | |
6 | ⊢ (f ∧ more) ; f+ ⊃ (g ∧ more) ; f+ | |
7 | ⊢ f+ ∧¬(g+) ⊃ ((g ∧ more) ; f+) ∧¬((g ∧ more) ; g+) | |
8 | ⊢ g ∧ more ⊃ more | |
9 | ⊢ f+ ⊃ g+ | |
qed
| ⊢ | f ≡ g ⇒ ⊢ f+ ≡ g+ | | ChopPlusEqvChopPlus |
Proof:
1 | ⊢ f ≡ g | given |
2 | ⊢ f ⊃ g | |
3 | ⊢ f+ ⊃ g+ | |
4 | ⊢ g ⊃ f | |
5 | ⊢ g+ ⊃ f+ | |
6 | ⊢ f+ ≡ g+ | |
qed
|
| |
Next