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

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024