BfMoreImpAndNextImpAndSkipAndChop

⊢

(more ⊃ f) ∧

g ⊃ (skip ∧ f) ⌢ g

Proof:

1	(more ⊃ f) ⊃ (skip ⊃ f)	BfMoreImpImpBfSkipImp
2	(skip ⊃ f) ∧ g ⊃ (skip ∧ f) ⌢ g	BfSkipImpAndNextImpAndSkipAndChop
3	(more ⊃ f) ∧ g ⊃ (skip ∧ f) ⌢ g	1, 2,Prop

qed

2023-09-12