valid_sentences.md

[1] pry(main)> Sequent.build('∀x.(P(x) => Q(x)) |- ∀x.(P(x) ∧ R(x) => Q(x) ∧ R(x))').show_lk_proof_figure
P(A) |- P(A)
------ (W R)
P(A) |- Q(A), P(A)
------ (W L)
P(A), R(A) |- Q(A), P(A)
------ (W L)
∀x.(P(x) => Q(x)), P(A), R(A) |- Q(A), P(A)
    Q(A) |- Q(A)
    ------ (W L)
    R(A), Q(A) |- Q(A)
    ------ (W L)
    P(A), R(A), Q(A) |- Q(A)
    ------ (W L)
    ∀x.(P(x) => Q(x)), P(A), R(A), Q(A) |- Q(A)
------ (=> L)
∀x.(P(x) => Q(x)), P(A), R(A), P(A) => Q(A) |- Q(A)
------ (∀ L)
∀x.(P(x) => Q(x)), P(A), R(A) |- Q(A)
    R(A) |- R(A)
    ------ (W L)
    P(A), R(A) |- R(A)
    ------ (W L)
    ∀x.(P(x) => Q(x)), P(A), R(A) |- R(A)
------ (∧ R)
∀x.(P(x) => Q(x)), P(A), R(A) |- Q(A) ∧ R(A)
------ (∧ L)
∀x.(P(x) => Q(x)), P(A) ∧ R(A) |- Q(A) ∧ R(A)
------ (=> R)
∀x.(P(x) => Q(x)) |- (P(A) ∧ R(A)) => (Q(A) ∧ R(A))
------ (∀ R)
∀x.(P(x) => Q(x)) |- ∀x.((P(x) ∧ R(x)) => (Q(x) ∧ R(x)))
=> nil
[2] pry(main)>

[1] pry(main)> Sequent.build('∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))) |- ∀x.(P(x) ∨ R(x))').show_lk_proof_figure
P(A) |- P(A)
------ (W R)
P(A) |- P(A), R(A)
------ (W L)
P(A), Q(A) |- P(A), R(A)
------ (W L)
∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))), P(A), Q(A) |- P(A), R(A)
------ (∧ L)
∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))), P(A) ∧ Q(A) |- P(A), R(A)
    R(A) |- R(A)
    ------ (W R)
    R(A) |- P(A), R(A)
    ------ (W L)
    R(A), S(A) |- P(A), R(A)
    ------ (W L)
    ∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))), R(A), S(A) |- P(A), R(A)
    ------ (∧ L)
    ∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))), R(A) ∧ S(A) |- P(A), R(A)
------ (∨ L)
∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))), (P(A) ∧ Q(A)) ∨ (R(A) ∧ S(A)) |- P(A), R(A)
------ (∀ L)
∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))) |- P(A), R(A)
------ (∨ R)
∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))) |- P(A) ∨ R(A)
------ (∀ R)
∀x.((P(x) ∧ Q(x)) ∨ (R(x) ∧ S(x))) |- ∀x.(P(x) ∨ R(x))
=> nil
[2] pry(main)>