git @ Cat's Eye Technologies Maxixe / master eg / sugared.maxixe
master

Tree @master (Download .tar.gz)

sugared.maxixe @master — raw · history · blame 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
given
    Modus_Ponens                 = impl(P, Q)    ; P           |- Q
    Modus_Tollens                = impl(P, Q)    ; not(Q)      |- not(P)
    Hypothetical_Syllogism       = impl(P, Q)    ; impl(Q, R)  |- impl(P, R)
    Disjunctive_Syllogism        = or(P, Q)      ; not(P)      |- Q
    Addition                     = P                           |- or(P, Q)
    Simplification               = P ∧ Q                       |- Q
    Conjunction                  = P             ; Q           |- P ∧ Q
    Resolution                   = or(not(P, R)) ; or(P, Q)    |- or(Q, R)

    Commutativity_of_Conjunction = P ∧ Q                       |- Q ∧ P

    Premise                      =                             |- p ∧ impl(p, q)
show
    q
proof
    Step_1 = p ∧ impl(p, q)                  by Premise
    Step_2 = impl(p, q) ∧ p                  by Commutativity_of_Conjunction with Step_1
    Step_3 = impl(p, q)                      by Simplification with Step_1
    Step_4 = p                               by Simplification with Step_2
    Step_5 = q                               by Modus_Ponens with Step_3, Step_4
qed