HaltChopAnd

(halt w) ; f (halt w) ; g (halt w) ; (f g) HaltChopAnd

Proof:

1
(halt w) ; g (halt w) g
2
(halt w) ; f (halt w) ; g (halt w) ; f (halt w) g
1, 2,Prop
3
(halt w) ; f (halt w) g (halt w) ; (f g)
4
(halt w) ; f (halt w) ; g (halt w) ; (f g)
2, 3,Prop

qed

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