| ⊢ | (f ⊃ g) ⊃ f∗ ⊃ g∗ | BaCSImpCS |
Proof:
1 | ⊢ f∗≡empty ∨ (f ∧more) ; f∗ | |
2 | ⊢ g∗≡empty ∨ (g ∧more) ; g∗ | |
3 | ⊢ f∗∧¬(g∗) ⊃ (f ∧more) ; f∗∧¬((g ∧more) ; g∗) | |
4 | ⊢ (f ⊃ g) ⊃ (f ∧more ⊃ g ∧more) | |
5 | ⊢ (f ⊃ g) ⊃ (f ∧more ⊃ g ∧more) | |
6 | ⊢ (f ∧more ⊃ g ∧more) ⊃ (f ∧more) ; f∗ ⊃ |
|
(g ∧more) ; f∗ | ||
7 | ⊢ (f ⊃ g) ∧ (f ∧more) ; f∗⊃ (g ∧more) ; f∗ | |
8 | ⊢ (g ∧more) ; f∗∧¬((g ∧more) ; g∗) ⊃ |
|
(g ∧more) ; (f∗∧¬(g∗)) | ||
9 | ⊢ (g ∧more) ; (f∗∧¬(g∗)) ⊃more ; (f∗∧¬(g∗)) | |
10 | ⊢ (f ⊃ g) ⊃more ; (f∗∧¬(g∗)) ⊃ |
|
more ; ( (f ⊃ g) ∧ f∗∧¬(g∗)) | ||
11 | ⊢ (f ⊃ g) ∧ f∗∧¬(g∗) ⊃ |
|
more ; ( (f ⊃ g) ∧ f∗∧¬(g∗)) | ||
12 | ⊢ ¬( (f ⊃ g) ∧ f∗∧¬(g∗)) | |
13 | ⊢ (f ⊃ g) ⊃ f∗ ⊃ g∗ | |
qed
The following corollary can be readily verified: