In [ ]:

```
// Load the Sylph package which contains the PropCalculus theory
// Run this cell first if there are any namespace errors when using this notebook.
#r "nuget: Sylph"
// Load helpers for the Jupyter .NET Core kernel.
#load "netcore.fsx"
```

In [3]:

```
open Sylvester
open PropCalculus
// Declare symbols we can reuse in formulae
let p,q,r = var3<bool>
```

In [38]:

```
// Theorem 3.2
let ``3.2`` = proof prop_calculus <@ p = p = q = q @> [
RightAssoc |> LR
def_true <@ q @> |> Trn |> R
Commute |> LR
]
```

In [5]:

```
// Theorem 3.4
let ``3.4`` = proof prop_calculus <@ true @> [
def_true <@ p @> |> LR
]
```

In [6]:

```
// Theorem 3.5
let ``3.5`` = axiom prop_calculus <@ p = p @>
```

[Lemma] p = p: ⊢ p = p. [Axiom of Symbolic Equality] Proof complete.

In [7]:

```
// Theorem 3.11
let ``3.11`` = proof prop_calculus <@ not p = q = p = not q @> [
Collect |> L
RightAssoc |> LR
Commute |> R
Collect |> R
Commute |> R
]
```

In [8]:

```
// Theorem 3.12
let ``3.12`` = proof prop_calculus <@ not (not p) = p @> [
Collect |> LR
def_false <@ p @> |> Trn |> LR
not_false |> Truth |> LR
]
```

In [9]:

```
// Theorem 3.13
let ``3.13``= proof prop_calculus <@not false = true@> [
Commute |> LR
def_true <@ false @> |> L
RightAssoc |> LR
Commute |> R
Collect |> R
def_true <@ false @> |> Trn |> R
]
```

In [10]:

```
// Theorem 3.14
let ``3.14`` = axiom prop_calculus <@ (p <> q) = not (p = q) @>
```

[Lemma] p <> q = ¬ (p = q): ⊢ p <> q = ¬ (p = q). [Definition of (<>)] Proof complete.

In [11]:

```
// Theorem 3.15
let ``3.15`` = proof prop_calculus <@ not p = p = false@> [
Collect |> L
def_true <@ p @> |> Trn |> L
Commute |> LR
]
```

In [12]:

```
// Theorem 3.16
let ``3.16`` = proof prop_calculus <@ (p <> q) = (q <> p) @> [
def_not_eq <@ p @> <@ q @> |> L
def_not_eq <@ q @> <@ p @> |> R
Commute |> R
]
```

In [13]:

```
// Theorem 3.17
let ``3.17`` =
proof prop_calculus <@ ((p <> q) <> r) = (p <> (q <> r)) @> [
def_not_eq <@ p @> <@ q @> |> L
def_not_eq <@ not (p = q) @> <@ r @> |> L
def_not_eq <@ q @> <@ r @> |> R
def_not_eq <@ p @> <@ not (q = r) @> |> R
distrib_not <@ q @> <@ r @> |> R
LeftAssoc |> R
commute_eq <@ p @> <@ not q @> |> R
collect_not <@ q @> <@ p @> |> R
commute_eq <@ q @> <@ p @> |> R
]
```

In [14]:

```
// Theorem 3.29
let ``3.29`` = proof prop_calculus <@ p ||| true = true @> [
def_true <@ p @> |> LR
Distrib |> LR
Idemp |> LR
]
```

In [15]:

```
// Theorem 3.30
let ``3.30`` = proof prop_calculus <@p ||| false = p @> [
def_false <@ p @> |> L
L Distrib
LR RightAssoc
R Idemp
L ExcludedMiddle
]
```

In [16]:

```
// Theorem 3.31
let ``3.31`` = proof prop_calculus <@ (p ||| (q ||| r)) = ((p ||| q) ||| (p ||| r)) @> [
commute_or_or <@ p @> <@ q @> <@ p @> <@ r @> |> R
idemp_or <@ p @> |> R
]
```

In [17]:

```
let ``3.32`` = proof prop_calculus <@ (p ||| q) = (p ||| not q = p) @> [
LeftAssoc |> LR
collect_or_eq <@ p @> <@ q @> <@ not q @> |> LR
commute_eq <@ q @> <@ not q @> |> L
def_false <@ q @> |> Trn |> L
ident_or <@ p @> |> L
]
```

In [18]:

```
let ``3.37`` = proof prop_calculus <@ (p |&| q |&| r) = (p |&| (q |&| r)) @> [
golden_rule <@ p @> <@ q @> |> L
golden_rule <@ (p = q) = (p ||| q) @> <@ r @> |> L
commute_or <@ ((p = q) = (p ||| q)) @> <@ r @> |> L
distrib_or_eq <@ r @> <@ p = q @> <@ p ||| q @> |> L
distrib_or_eq <@ r @> <@ p @> <@ q @> |> L
right_assoc_eq <@ p = q@> <@ p ||| q@> <@ r @> |> L
commute_eq <@ p ||| q @> <@ r @> |> L
commute_or <@ r @> <@ q @> |> L
commute_eq <@ r ||| p@> <@ q ||| r@> |> L
commute_or <@ r @> <@ p ||| q @> |> L
L LeftAssoc
L LeftAssoc
L LeftAssoc
commute_and <@ p @> <@ q |&| r @> |> R
ident_and_eq_all <@ q @> <@ r @> <@ p @> |> R
commute_eq <@q = r@> <@ p @> |> R
]
```

In [19]:

```
let ``3.38`` = proof prop_calculus <@ (p |&| p) = p @> [
LR GoldenRule
RightAssoc |> LR
idemp_or <@ p @> |> Taut |> R
LR Commute
]
```

In [20]:

```
let ``3.39`` = proof prop_calculus <@ (p |&| true) = p @> [
LR GoldenRule
LR RightAssoc
zero_or <@ p @> |> R
R Commute
]
```

In [21]:

```
let ``3.40`` = proof prop_calculus <@ (p |&| false) = false @> [
LR GoldenRule
ident_or <@ p @> |> L
LR RightAssoc
]
```

In [22]:

```
// Theorem 3.41
let ``3.41`` = proof prop_calculus <@ (p |&| (q |&| r)) = ((p |&| q) |&| (p |&| r)) @> [
LeftAssoc |> R
right_assoc_and <@ p @> <@ q @> <@ p @> |> R
commute_and <@ q @> <@ p @> |> R
LeftAssoc |> R
idemp_and <@ p @> |> R
LeftAssoc |> L
]
```

[Lemma] p ∧ q = (p = q = p ∨ q): ⊢ p ∧ q = (p = q = p ∨ q). [Axiom of the Golden Rule] Proof complete. [Lemma] PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q ∧ p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q = p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q) ∨ p): ⊢ PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q ∧ p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q = p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q) ∨ p). [Axiom of the Golden Rule] Proof complete. [Lemma] (p = q = p ∨ q) ∨ p = p ∨ (p = q = p ∨ q): ⊢ (p = q = p ∨ q) ∨ p = p ∨ (p = q = p ∨ q). [Axiom of Commutativity] Proof complete. [Lemma] p ∨ (p = q = p ∨ q) = (p ∨ (p = q) = p ∨ (p ∨ q)): ⊢ p ∨ (p = q = p ∨ q) = (p ∨ (p = q) = p ∨ (p ∨ q)). [Axiom of Distributivity] Proof complete. [Lemma] p ∨ (p = q) = (p ∨ p = p ∨ q): ⊢ p ∨ (p = q) = (p ∨ p = p ∨ q). [Axiom of Distributivity] Proof complete. [Lemma] p = q = (p ∨ q = p) = (p = q = p ∨ q = p): 1. Logical operators in right of expression are right-associative: p = q = (p ∨ q = p) = (p = q = p ∨ q = p) → p = q = (p ∨ q = p) = (p = q = (p ∨ q = p)). ⊢ p = q = (p ∨ q = p) = (p = q = (p ∨ q = p)). [Axiom of Symbolic Equality] Proof complete. [Lemma] p = q = p ∨ q = p = (p = q = (p ∨ q = p)): ⊢ p = q = p ∨ q = p = (p = q = (p ∨ q = p)). [Axiom of Associativity] Proof complete. [Lemma] p ∨ q = p = (p = p ∨ q): 1. Logical operators in expression are left-associative: p ∨ q = p = (p = p ∨ q) → p ∨ q = p = p = p ∨ q. ⊢ p ∨ q = p = p = p ∨ q. [Axiom of Symmetry] Proof complete. [Lemma] p ∨ q = q ∨ p: ⊢ p ∨ q = q ∨ p. [Axiom of Commutativity] Proof complete. [Lemma] p ∨ p = q ∨ p = (q ∨ p = p ∨ p): 1. Logical operators in expression are left-associative: p ∨ p = q ∨ p = (q ∨ p = p ∨ p) → p ∨ p = q ∨ p = q ∨ p = p ∨ p. ⊢ p ∨ p = q ∨ p = q ∨ p = p ∨ p. [Axiom of Symmetry] Proof complete. [Lemma] p ∨ (p ∨ q) = p ∨ q ∨ p: ⊢ p ∨ (p ∨ q) = p ∨ q ∨ p. [Axiom of Commutativity] Proof complete. [Lemma] (q ∧ p) ∨ p = p ∨ (q ∧ p): ⊢ (q ∧ p) ∨ p = p ∨ (q ∧ p). [Axiom of Commutativity] Proof complete. [Lemma] q ∧ p = p = (p = (q ∧ p)): 1. Logical operators in expression are left-associative: q ∧ p = p = (p = (q ∧ p)) → q ∧ p = p = p = (q ∧ p). ⊢ q ∧ p = p = p = (q ∧ p). [Axiom of Symmetry] Proof complete. [Lemma] p ∧ (q ∧ p) = (q ∧ p ∧ p): 1. Logical terms in expression satisfy the golden rule: p ∧ (q ∧ p) = (q ∧ p ∧ p) → p = (q ∧ p) = p ∨ (q ∧ p) = (q ∧ p = p = (q ∧ p) ∨ p). Proof incomplete. Current state: p = (q ∧ p) = p ∨ (q ∧ p) = (q ∧ p = p = (q ∧ p) ∨ p). 2. Substitute (q ∧ p) ∨ p ≡ p ∨ (q ∧ p) into right of expression. Proof incomplete. Current state: p = (q ∧ p) = p ∨ (q ∧ p) = (q ∧ p = p = p ∨ (q ∧ p)). 3. Substitute q ∧ p = p ≡ p = (q ∧ p) into right of expression. ⊢ p = (q ∧ p) = p ∨ (q ∧ p) = (p = (q ∧ p) = p ∨ (q ∧ p)). [Axiom of Symbolic Equality] Proof complete. [Lemma] q ∧ p = (q = p = q ∨ p): ⊢ q ∧ p = (q = p = q ∨ p). [Axiom of the Golden Rule] Proof complete. [Lemma] q = p = q ∨ p ∧ p = (q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p): ⊢ q = p = q ∨ p ∧ p = (q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p). [Axiom of the Golden Rule] Proof complete. [Lemma] (q = p = q ∨ p) ∨ p = p ∨ (q = p = q ∨ p): ⊢ (q = p = q ∨ p) ∨ p = p ∨ (q = p = q ∨ p). [Axiom of Commutativity] Proof complete. [Lemma] p ∨ (q = p = q ∨ p) = (p ∨ (q = p) = p ∨ (q ∨ p)): ⊢ p ∨ (q = p = q ∨ p) = (p ∨ (q = p) = p ∨ (q ∨ p)). [Axiom of Distributivity] Proof complete. [Lemma] p ∨ (q = p) = (p ∨ q = p ∨ p): ⊢ p ∨ (q = p) = (p ∨ q = p ∨ p). [Axiom of Distributivity] Proof complete. [Lemma] q = p = (q ∨ p = p) = (q = p = q ∨ p = p): 1. Logical operators in right of expression are right-associative: q = p = (q ∨ p = p) = (q = p = q ∨ p = p) → q = p = (q ∨ p = p) = (q = p = (q ∨ p = p)). ⊢ q = p = (q ∨ p = p) = (q = p = (q ∨ p = p)). [Axiom of Symbolic Equality] Proof complete. [Lemma] q = p = q ∨ p = p = (q = p = (q ∨ p = p)): ⊢ q = p = q ∨ p = p = (q = p = (q ∨ p = p)). [Axiom of Associativity] Proof complete. [Lemma] q ∨ p = p = (p = q ∨ p): 1. Logical operators in expression are left-associative: q ∨ p = p = (p = q ∨ p) → q ∨ p = p = p = q ∨ p. ⊢ q ∨ p = p = p = q ∨ p. [Axiom of Symmetry] Proof complete. [Lemma] p ∨ p = p ∨ p: ⊢ p ∨ p = p ∨ p. [Axiom of Symbolic Equality] Proof complete. [Lemma] p ∨ q = p ∨ p = (p ∨ p = p ∨ q): 1. Logical operators in expression are left-associative: p ∨ q = p ∨ p = (p ∨ p = p ∨ q) → p ∨ q = p ∨ p = p ∨ p = p ∨ q. ⊢ p ∨ q = p ∨ p = p ∨ p = p ∨ q. [Axiom of Symmetry] Proof complete. [Lemma] p ∨ (q ∨ p) = q ∨ p ∨ p: ⊢ p ∨ (q ∨ p) = q ∨ p ∨ p. [Axiom of Commutativity] Proof complete. [Lemma] q ∧ p ∧ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p): 1. Substitute q ∧ p ≡ q = p = q ∨ p into left of expression. Proof incomplete. Current state: q = p = q ∨ p ∧ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 2. Substitute q = p = q ∨ p ∧ p ≡ q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p into left of expression. Proof incomplete. Current state: q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 3. Substitute (q = p = q ∨ p) ∨ p ≡ p ∨ (q = p = q ∨ p) into left of expression. Proof incomplete. Current state: q = p = q ∨ p = p = p ∨ (q = p = q ∨ p) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 4. Substitute p ∨ (q = p = q ∨ p) ≡ p ∨ (q = p) = p ∨ (q ∨ p) into left of expression. Proof incomplete. Current state: q = p = q ∨ p = p = (p ∨ (q = p) = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 5. Substitute p ∨ (q = p) ≡ p ∨ q = p ∨ p into left of expression. Proof incomplete. Current state: q = p = q ∨ p = p = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 6. Substitute q = p = q ∨ p = p ≡ q = p = (q ∨ p = p) into left of expression. Proof incomplete. Current state: q = p = (q ∨ p = p) = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 7. Substitute q ∨ p = p ≡ p = q ∨ p into left of expression. Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 8. Substitute p ∨ p ≡ p ∨ p into expression: No change. Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 9. Substitute p ∨ q = p ∨ p ≡ p ∨ p = p ∨ q into left of expression. Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 10. Substitute p ∨ (q ∨ p) ≡ q ∨ p ∨ p into left of expression. Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q = q ∨ p ∨ p) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 11. Logical operators in left of expression are left-associative: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q = q ∨ p ∨ p) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p) → q = p = (p = q ∨ p) = (p ∨ p = p ∨ q) = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q) = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 12. Logical operators in left of expression are left-associative: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q) = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p) → q = p = (p = q ∨ p) = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). Proof incomplete. Current state: q = p = (p = q ∨ p) = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). 13. Logical operators in left of expression are left-associative: q = p = (p = q ∨ p) = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p) → q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). ⊢ q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). [Axiom of Symbolic Equality] Proof complete. [Lemma] q = p = p = (p = (q = p)): 1. Logical operators in expression are left-associative: q = p = p = (p = (q = p)) → q = p = p = p = (q = p). ⊢ q = p = p = p = (q = p). [Axiom of Symmetry] Proof complete. [Lemma] p = (q = p) = (p = q = p): 1. Logical operators in right of expression are right-associative: p = (q = p) = (p = q = p) → p = (q = p) = (p = (q = p)). ⊢ p = (q = p) = (p = (q = p)). [Axiom of Symbolic Equality] Proof complete. [Lemma] q ∨ p ∨ p = p ∨ (q ∨ p): ⊢ q ∨ p ∨ p = p ∨ (q ∨ p). [Axiom of Commutativity] Proof complete. [Lemma] p ∨ (q ∨ p) = p ∨ q ∨ p: 1. Logical operators in expression are left-associative: p ∨ (q ∨ p) = p ∨ q ∨ p → p ∨ q ∨ p = p ∨ q ∨ p. ⊢ p ∨ q ∨ p = p ∨ q ∨ p. [Axiom of Symbolic Equality] Proof complete. [Lemma] p = q = p = (q ∨ p = p ∨ p) = (p = q = p = q ∨ p = p ∨ p): 1. Logical operators in right of expression are right-associative: p = q = p = (q ∨ p = p ∨ p) = (p = q = p = q ∨ p = p ∨ p) → p = q = p = (q ∨ p = p ∨ p) = (p = q = p = (q ∨ p = p ∨ p)). ⊢ p = q = p = (q ∨ p = p ∨ p) = (p = q = p = (q ∨ p = p ∨ p)). [Axiom of Symbolic Equality] Proof complete. [Lemma] p = q = p = q ∨ p = p ∨ p = (p = q = p = (q ∨ p = p ∨ p)): ⊢ p = q = p = q ∨ p = p ∨ p = (p = q = p = (q ∨ p = p ∨ p)). [Axiom of Associativity] Proof complete. [Lemma] p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ p = p ∨ q): 1. Logical operators in right of expression are right-associative: p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ p = p ∨ q) → p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)). ⊢ p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)). [Axiom of Symbolic Equality] Proof complete. [Lemma] p = q = p = q ∨ p = p ∨ p = p ∨ q = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)): ⊢ p = q = p = q ∨ p = p ∨ p = p ∨ q = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)). [Axiom of Associativity] Proof complete. [Lemma] p ∨ p = p ∨ q = (p ∨ q = p ∨ p): 1. Logical operators in expression are left-associative: p ∨ p = p ∨ q = (p ∨ q = p ∨ p) → p ∨ p = p ∨ q = p ∨ q = p ∨ p. ⊢ p ∨ p = p ∨ q = p ∨ q = p ∨ p. [Axiom of Symmetry] Proof complete. [Lemma] p = q = p = (q ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ q): 1. Logical operators in right of expression are right-associative: p = q = p = (q ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ q) → p = q = p = (q ∨ p = p ∨ q) = (p = q = p = (q ∨ p = p ∨ q)). ⊢ p = q = p = (q ∨ p = p ∨ q) = (p = q = p = (q ∨ p = p ∨ q)). [Axiom of Symbolic Equality] Proof complete. [Lemma] p = q = p = q ∨ p = p ∨ q = (p = q = p = (q ∨ p = p ∨ q)): ⊢ p = q = p = q ∨ p = p ∨ q = (p = q = p = (q ∨ p = p ∨ q)). [Axiom of Associativity] Proof complete. [Lemma] q ∨ p = p ∨ q = (p ∨ q = q ∨ p): 1. Logical operators in expression are left-associative: q ∨ p = p ∨ q = (p ∨ q = q ∨ p) → q ∨ p = p ∨ q = p ∨ q = q ∨ p. ⊢ q ∨ p = p ∨ q = p ∨ q = q ∨ p. [Axiom of Symmetry] Proof complete.

Unhandled Exception The expression p |&| q |&| p = p |&| (q |&| p) is not an identity at Microsoft.FSharp.Core.PrintfModule.PrintFormatToStringThenFail@1637.Invoke(String message) in F:\workspace.1\_work\1\s\src\fsharp\FSharp.Core\printf.fs:line 1637 at Sylvester.ProofModule.ident[t](Theory theory, FSharpExpr`1 e, FSharpList`1 steps) at Sylvester.PropCalculus.right_assoc_and(FSharpExpr`1 p, FSharpExpr`1 q, FSharpExpr`1 r) at <StartupCode$FSI_0027>.$FSI_0027.main@()

In [23]:

```
let ``3.42`` = proof prop_calculus <@p |&| not p = false@> [
GoldenRule |> L
ExcludedMiddle |> L
commute_eq <@ p @> <@ not p @> |> L
def_false <@ p @> |> Trn |> L
commute_eq <@ false @> <@ true @> |> L
RightAssoc |> LR
]
```

In [24]:

```
let ``3.43a`` = proof prop_calculus <@ (p |&| (p ||| q)) = p @> [
GoldenRule |> L
left_assoc_or <@ p @> <@ p @> <@ q @> |> L
idemp_or <@ p @> |> L
]
```

In [25]:

```
let ``3.43b`` = proof prop_calculus <@ (p ||| (p |&| q)) = p @> [
GoldenRule |> L
Distrib |> L
left_assoc_or <@ p @> <@ p @> <@ q @> |> L
idemp_or <@ p @> |> L
Distrib |> L
idemp_or <@ p @> |> L
]
```

In [37]:

```
let ``3.44a`` = proof prop_calculus <@ p |&| (not p ||| q) = (p |&| q) @> [
GoldenRule |> L
left_assoc_or <@ p @> <@ not p @> <@ q @> |> L
ExcludedMiddle |> L
zero_or <@ q @> |> TrnL |> L
ident_eq <@ p = (not p ||| q) @> |> L
commute_or <@ not p@> <@ q @> |> L
ident_or_not_or <@ q @> <@ p @> |> L
LeftAssoc |> L
commute_or <@ q @> <@ p @> |> L
golden_rule <@ p @> <@ q @> |> Trn |> L
]
```