2013-11-29 05:48:30 +00:00
|
|
|
Set: pp::colors
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
Assumed: p
|
|
|
|
|
Assumed: q
|
|
|
|
|
Assumed: r
|
|
|
|
|
Proved: T1
|
|
|
|
|
Proved: T2
|
|
|
|
|
Theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H (Conj H::1 H)))
|
|
|
|
|
Proved: T3
|
|
|
|
|
Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
|
|
|
|
|
Discharge
|
|
|
|
|
(λ H : p,
|
2013-12-07 00:31:13 +00:00
|
|
|
Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))
|
2013-12-26 23:54:53 +00:00
|
|
|
Proved: T4
|
|
|
|
|
Theorem T4 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
|
|
|
|
|
Discharge
|
|
|
|
|
(λ H : p,
|
|
|
|
|
Discharge
|
|
|
|
|
(λ H::1 : p ∧ q,
|
|
|
|
|
Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (let H::1::1 := Conjunct1 H::1 in Conj H::2 H::1::1))))
|
