NextChop

( f) ⌢ g (f ⌢ g) NextChop

Proof:

1
(skip ⌢ f) ⌢ g skip (f ⌢ g)
2
( f) ⌢ g (f ⌢ g)
1, def. of 

qed

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023