StateImpYields

w f fin w1 ⇒ ⊢ w (f w1) StateImpYields

Proof:

1
w f fin w1
given
2
w (f fin w1)
1,Prop
3
w (f fin w1)
4
(f fin w1) f w1
5
w (f w1)
3, 4,EqvChain

qed

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