Beginning of Section Alg

Variable extension_tag : set

Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha extension_tag

Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.

Definition. We define pair_tag to be λx y ⇒ x ∪ {u ''|u ∈ y} of type set → set → set.

In Proofgold the corresponding term root is abc4d9... and object id is 76732f...

Variable F : set → prop

Hypothesis extension_tag_fresh : ∀x, F x → ∀u ∈ x, extension_tag ∉ u

Theorem. (ctagged_notin_F)

∀x y, F x → (y '') ∉ x

In Proofgold the corresponding term root is 67cee9... and proposition id is 8b7e9e...

Proof:

Let x and y be given.

Assume Hx: F x.

Assume H1: y '' ∈ x.

Apply extension_tag_fresh x Hx (y '') H1 to the current goal.

We will prove extension_tag ∈ y ''.

We will prove extension_tag ∈ y ∪ {extension_tag}.

Apply binunionI2 to the current goal.

Apply SingI to the current goal.

∎

Theorem. (ctagged_eqE_Subq)

∀x y, F x → ∀u ∈ x, ∀v, u '' = v '' → u ⊆ v

In Proofgold the corresponding term root is a506f8... and proposition id is cbce18...

Proof:

Let x and y be given.

Assume Hx.

Let u be given.

Assume Hu.

Let v be given.

Assume Huv.

Let w be given.

Assume Hw: w ∈ u.

We prove the intermediate claim L1: w ∈ v ''.

rewrite the current goal using Huv (from right to left).

We will prove w ∈ u ∪ {extension_tag}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hw.

Apply binunionE v {extension_tag} w L1 to the current goal.

Assume H1: w ∈ v.

An exact proof term for the current goal is H1.

Assume H1: w ∈ {extension_tag}.

We will prove False.

We prove the intermediate claim L2: w = extension_tag.

An exact proof term for the current goal is SingE extension_tag w H1.

Apply extension_tag_fresh x Hx u Hu to the current goal.

We will prove extension_tag ∈ u.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is Hw.

∎

Theorem. (ctagged_eqE_eq)

∀x y, F x → F y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u = v

In Proofgold the corresponding term root is 80ff51... and proposition id is 397f7d...

Proof:

Let x and y be given.

Assume Hx Hy.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv Huv.

Apply set_ext to the current goal.

An exact proof term for the current goal is ctagged_eqE_Subq x y Hx u Hu v Huv.

Apply ctagged_eqE_Subq y x Hy v Hv u to the current goal.

Use symmetry.

An exact proof term for the current goal is Huv.

∎

Theorem. (pair_tag_prop_1_Subq)

∀x1 y1 x2 y2, F x1 → pair_tag x1 y1 = pair_tag x2 y2 → x1 ⊆ x2

In Proofgold the corresponding term root is 7d9199... and proposition id is a3ef42...

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hx1.

Assume H1: pair_tag x1 y1 = pair_tag x2 y2.

Let v be given.

Assume Hv: v ∈ x1.

We prove the intermediate claim L1: v ∈ pair_tag x2 y2.

rewrite the current goal using H1 (from right to left).

We will prove v ∈ x1 ∪ {u ''|u ∈ y1}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hv.

Apply binunionE x2 {u ''|u ∈ y2} v L1 to the current goal.

Assume H2: v ∈ x2.

An exact proof term for the current goal is H2.

Assume H2: v ∈ {u ''|u ∈ y2}.

We will prove False.

Apply ReplE_impred y2 (λu ⇒ u '') v H2 to the current goal.

Let u be given.

Assume Hu: u ∈ y2.

Assume Hvu: v = u ''.

Apply ctagged_notin_F x1 u Hx1 to the current goal.

We will prove u '' ∈ x1.

rewrite the current goal using Hvu (from right to left).

An exact proof term for the current goal is Hv.

∎

Theorem. (pair_tag_prop_1)

∀x1 y1 x2 y2, F x1 → F x2 → pair_tag x1 y1 = pair_tag x2 y2 → x1 = x2

In Proofgold the corresponding term root is 6d65de... and proposition id is a92ff7...

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hx1 Hx2.

Assume H1: pair_tag x1 y1 = pair_tag x2 y2.

Apply set_ext to the current goal.

An exact proof term for the current goal is pair_tag_prop_1_Subq x1 y1 x2 y2 Hx1 H1.

Apply pair_tag_prop_1_Subq x2 y2 x1 y1 Hx2 to the current goal.

Use symmetry.

An exact proof term for the current goal is H1.

∎

Theorem. (pair_tag_prop_2_Subq)

∀x1 y1 x2 y2, F y1 → F x2 → F y2 → pair_tag x1 y1 = pair_tag x2 y2 → y1 ⊆ y2

In Proofgold the corresponding term root is 51b765... and proposition id is f24efc...

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hy1 Hx2 Hy2.

Assume H1: pair_tag x1 y1 = pair_tag x2 y2.

Let v be given.

Assume Hv: v ∈ y1.

We prove the intermediate claim L1: v '' ∈ pair_tag x2 y2.

rewrite the current goal using H1 (from right to left).

We will prove v '' ∈ x1 ∪ {u ''|u ∈ y1}.

Apply binunionI2 to the current goal.

We will prove v '' ∈ {u ''|u ∈ y1}.

An exact proof term for the current goal is ReplI y1 (λu ⇒ u '') v Hv.

Apply binunionE x2 {u ''|u ∈ y2} (v '') L1 to the current goal.

Assume H2: v '' ∈ x2.

We will prove False.

An exact proof term for the current goal is ctagged_notin_F x2 v Hx2 H2.

Assume H2: v '' ∈ {u ''|u ∈ y2}.

Apply ReplE_impred y2 (λu ⇒ u '') (v '') H2 to the current goal.

Let u be given.

Assume Hu: u ∈ y2.

Assume Hvu: v '' = u ''.

We prove the intermediate claim L2: v = u.

An exact proof term for the current goal is ctagged_eqE_eq y1 y2 Hy1 Hy2 v Hv u Hu Hvu.

We will prove v ∈ y2.

rewrite the current goal using L2 (from left to right).

An exact proof term for the current goal is Hu.

∎

Theorem. (pair_tag_prop_2)

∀x1 y1 x2 y2, F x1 → F y1 → F x2 → F y2 → pair_tag x1 y1 = pair_tag x2 y2 → y1 = y2

In Proofgold the corresponding term root is 5f9628... and proposition id is e5fc85...

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hx1 Hy1 Hx2 Hy2.

Assume H1: pair_tag x1 y1 = pair_tag x2 y2.

Apply set_ext to the current goal.

An exact proof term for the current goal is pair_tag_prop_2_Subq x1 y1 x2 y2 Hy1 Hx2 Hy2 H1.

Apply pair_tag_prop_2_Subq x2 y2 x1 y1 Hy2 Hx1 Hy1 to the current goal.

Use symmetry.

An exact proof term for the current goal is H1.

∎

Theorem. (pair_tag_0)

∀x, pair_tag x 0 = x

In Proofgold the corresponding term root is 67646d... and proposition id is 38d429...

Proof:

Let x be given.

We will prove x ∪ {u ''|u ∈ 0} = x.

rewrite the current goal using Repl_Empty (λu ⇒ u '') (from left to right).

We will prove x ∪ 0 = x.

An exact proof term for the current goal is binunion_idr x.

∎

Definition. We define CD_carr to be λz ⇒ ∃x, F x ∧ ∃y, F y ∧ z = pair_tag x y of type set → prop.

In Proofgold the corresponding term root is 0c2c09... and object id is 787a60...

Theorem. (CD_carr_I)

∀x y, F x → F y → CD_carr (pair_tag x y)

In Proofgold the corresponding term root is 7da562... and proposition id is ff1d14...

Proof:

Let x and y be given.

Assume Hx Hy.

We will prove ∃x', F x' ∧ ∃y', F y' ∧ pair_tag x y = pair_tag x' y'.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

Use reflexivity.

∎

Theorem. (CD_carr_E)

∀z, CD_carr z → ∀p : set → prop, (∀x y, F x → F y → z = pair_tag x y → p (pair_tag x y)) → p z

In Proofgold the corresponding term root is 6d3181... and proposition id is 72fbc5...

Proof:

Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply Hz to the current goal.

Let x be given.

Assume H1.

Apply H1 to the current goal.

Assume Hx.

Assume H1.

Apply H1 to the current goal.

Let y be given.

Assume H1.

Apply H1 to the current goal.

Assume Hy Hzxy.

rewrite the current goal using Hzxy (from left to right).

An exact proof term for the current goal is Hp x y Hx Hy Hzxy.

∎

Theorem. (CD_carr_0ext)

F 0 → ∀x, F x → CD_carr x

In Proofgold the corresponding term root is 0fb20d... and proposition id is ed952a...

Proof:

Assume H0.

Let x be given.

Assume Hx.

We will prove ∃x', F x' ∧ ∃y, F y ∧ x = pair_tag x' y.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H0.

Use symmetry.

An exact proof term for the current goal is pair_tag_0 x.

∎

Definition. We define CD_proj0 to be λz ⇒ Eps_i (λx ⇒ F x ∧ ∃y, F y ∧ z = pair_tag x y) of type set → set.

In Proofgold the corresponding term root is e6d3c9... and object id is 672bda...

Definition. We define CD_proj1 to be λz ⇒ Eps_i (λy ⇒ F y ∧ z = pair_tag (CD_proj0 z) y) of type set → set.

In Proofgold the corresponding term root is 934eed... and object id is e1c3ce...

Let proj0 ≝ CD_proj0

Let proj1 ≝ CD_proj1

Let pa : set → set → set ≝ pair_tag

Theorem. (CD_proj0_1)

∀z, CD_carr z → F (proj0 z) ∧ ∃y, F y ∧ z = pa (proj0 z) y

In Proofgold the corresponding term root is cd8c23... and proposition id is e9b94d...

Proof:

Let z be given.

Assume Hz.

Apply Eps_i_ex (λx ⇒ F x ∧ ∃y, F y ∧ z = pa x y) to the current goal.

We will prove ∃x, F x ∧ ∃y, F y ∧ z = pa x y.

An exact proof term for the current goal is Hz.

∎

Theorem. (CD_proj0_2)

∀x y, F x → F y → proj0 (pa x y) = x

In Proofgold the corresponding term root is 58ae60... and proposition id is d0a094...

Proof:

Let x and y be given.

Assume Hx Hy.

Apply CD_proj0_1 (pa x y) (CD_carr_I x y Hx Hy) to the current goal.

Assume H1: F (proj0 (pa x y)).

Assume H2: ∃y', F y' ∧ pa x y = pa (proj0 (pa x y)) y'.

Apply H2 to the current goal.

Let y' be given.

Assume H3.

Apply H3 to the current goal.

Assume Hy': F y'.

Assume H4: pa x y = pa (proj0 (pa x y)) y'.

Use symmetry.

An exact proof term for the current goal is pair_tag_prop_1 x y (proj0 (pa x y)) y' Hx H1 H4.

∎

Theorem. (CD_proj1_1)

∀z, CD_carr z → F (proj1 z) ∧ z = pa (proj0 z) (proj1 z)

In Proofgold the corresponding term root is 29b7ad... and proposition id is da2481...

Proof:

Let z be given.

Assume Hz.

Apply Eps_i_ex (λy ⇒ F y ∧ z = pa (proj0 z) y) to the current goal.

We will prove ∃y, F y ∧ z = pa (proj0 z) y.

Apply CD_carr_E z Hz to the current goal.

Let x and y be given.

Assume Hx Hy.

Assume Hzxy: z = pa x y.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

We will prove pa x y = pa (proj0 (pa x y)) y.

Apply CD_proj0_2 x y Hx Hy (λu v ⇒ pa x y = pa v y) to the current goal.

We will prove pa x y = pa x y.

Use reflexivity.

∎

Theorem. (CD_proj1_2)

∀x y, F x → F y → proj1 (pa x y) = y

In Proofgold the corresponding term root is 582e7f... and proposition id is 006468...

Proof:

Let x and y be given.

Assume Hx Hy.

Use symmetry.

Apply CD_proj1_1 (pa x y) (CD_carr_I x y Hx Hy) to the current goal.

Assume H1: F (proj1 (pa x y)).

Apply CD_proj0_2 x y Hx Hy (λu v ⇒ pa x y = pa v (proj1 (pa x y)) → y = proj1 (pa x y)) to the current goal.

Assume H2: pa x y = pa x (proj1 (pa x y)).

An exact proof term for the current goal is pair_tag_prop_2 x y x (proj1 (pa x y)) Hx Hy Hx H1 H2.

∎

Theorem. (CD_proj0R)

∀z, CD_carr z → F (proj0 z)

In Proofgold the corresponding term root is db089e... and proposition id is 0344a9...

Proof:

Let z be given.

Assume Hz.

Apply CD_proj0_1 z Hz to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎

Theorem. (CD_proj1R)

∀z, CD_carr z → F (proj1 z)

In Proofgold the corresponding term root is 79b5f6... and proposition id is 197fac...

Proof:

Let z be given.

Assume Hz.

Apply CD_proj1_1 z Hz to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎

Theorem. (CD_proj0proj1_eta)

∀z, CD_carr z → z = pa (proj0 z) (proj1 z)

In Proofgold the corresponding term root is 005546... and proposition id is 9f625c...

Proof:

Let z be given.

Assume Hz.

Apply CD_proj1_1 z Hz to the current goal.

An exact proof term for the current goal is (λ_ H ⇒ H).

∎

Theorem. (CD_proj0proj1_split)

∀z w, CD_carr z → CD_carr w → proj0 z = proj0 w → proj1 z = proj1 w → z = w

In Proofgold the corresponding term root is de0617... and proposition id is 6f6778...

Proof:

Let z and w be given.

Assume Hz Hw.

Assume H1 H2.

Use transitivity with and (pa (proj0 z) (proj1 z)).

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

Use transitivity with and (pa (proj0 w) (proj1 w)).

rewrite the current goal using H1 (from left to right).

rewrite the current goal using H2 (from left to right).

Use reflexivity.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta w Hw.

∎

Theorem. (CD_proj0_F)

F 0 → ∀x, F x → CD_proj0 x = x

In Proofgold the corresponding term root is b4c9a8... and proposition id is 0324b7...

Proof:

Assume H0.

Let x be given.

Assume Hx.

rewrite the current goal using pair_tag_0 x (from right to left) at position 1.

We will prove CD_proj0 (pair_tag x 0) = x.

An exact proof term for the current goal is CD_proj0_2 x 0 Hx H0.

∎

Theorem. (CD_proj1_F)

F 0 → ∀x, F x → CD_proj1 x = 0

In Proofgold the corresponding term root is 40d7ac... and proposition id is 0861dd...

Proof:

Assume H0.

Let x be given.

Assume Hx.

rewrite the current goal using pair_tag_0 x (from right to left) at position 1.

We will prove CD_proj1 (pair_tag x 0) = 0.

An exact proof term for the current goal is CD_proj1_2 x 0 Hx H0.

∎

Beginning of Section CD_minus_conj

Variable minus : set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Definition. We define CD_minus to be λz ⇒ pa (- proj0 z) (- proj1 z) of type set → set.

In Proofgold the corresponding term root is 2d3588... and object id is 87e4d7...

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus.

Variable conj : set → set

Definition. We define CD_conj to be λz ⇒ pa (conj (proj0 z)) (- proj1 z) of type set → set.

In Proofgold the corresponding term root is b39bd2... and object id is 05d4c2...

End of Section CD_minus_conj

Beginning of Section CD_add

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Definition. We define CD_add to be λz w ⇒ pa (proj0 z + proj0 w) (proj1 z + proj1 w) of type set → set → set.

In Proofgold the corresponding term root is 7a5ff6... and object id is ac7808...

End of Section CD_add

Beginning of Section CD_mul

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Definition. We define CD_mul to be λz w ⇒ pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) of type set → set → set.

In Proofgold the corresponding term root is f53b0e... and object id is a0aea9...

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul.

Definition. We define CD_exp_nat to be λz m ⇒ nat_primrec 1 (λ_ r ⇒ z ⨯ r) m of type set → set → set.

In Proofgold the corresponding term root is 7fdc79... and object id is 750c11...

End of Section CD_mul

Beginning of Section CD_minus_conj_clos

Variable minus : set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Hypothesis F_minus : ∀x, F x → F (- x)

Theorem. (CD_minus_CD)

∀z, CD_carr z → CD_carr (:-: z)

In Proofgold the corresponding term root is 04b152... and proposition id is e2afae...

Proof:

Let z be given.

Assume Hz.

We will prove CD_carr (pa (- proj0 z) (- proj1 z)).

Apply CD_carr_I to the current goal.

Apply F_minus to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply F_minus to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

∎

Theorem. (CD_minus_proj0)

∀z, CD_carr z → proj0 (:-: z) = - proj0 z

In Proofgold the corresponding term root is 746fe1... and proposition id is ad320c...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove proj0 (pa (- proj0 z) (- proj1 z)) = - proj0 z.

An exact proof term for the current goal is CD_proj0_2 (- proj0 z) (- proj1 z) ?? ??.

∎

Theorem. (CD_minus_proj1)

∀z, CD_carr z → proj1 (:-: z) = - proj1 z

In Proofgold the corresponding term root is 93a203... and proposition id is 4e5c97...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove proj1 (pa (- proj0 z) (- proj1 z)) = - proj1 z.

An exact proof term for the current goal is CD_proj1_2 (- proj0 z) (- proj1 z) ?? ??.

∎

Variable conj : set → set

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Hypothesis F_conj : ∀x, F x → F (conj x)

Theorem. (CD_conj_CD)

∀z, CD_carr z → CD_carr (z ')

In Proofgold the corresponding term root is 78d930... and proposition id is 541129...

Proof:

Let z be given.

Assume Hz.

We will prove CD_carr (pa (conj (proj0 z)) (- proj1 z)).

Apply CD_carr_I to the current goal.

Apply F_conj to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply F_minus to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

∎

Theorem. (CD_conj_proj0)

∀z, CD_carr z → proj0 (z ') = conj (proj0 z)

In Proofgold the corresponding term root is a61a2e... and proposition id is 2104b7...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove proj0 (pa (conj (proj0 z)) (- proj1 z)) = conj (proj0 z).

An exact proof term for the current goal is CD_proj0_2 (conj (proj0 z)) (- proj1 z) ?? ??.

∎

Theorem. (CD_conj_proj1)

∀z, CD_carr z → proj1 (z ') = - proj1 z

In Proofgold the corresponding term root is c56033... and proposition id is 2bf262...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove proj1 (pa (conj (proj0 z)) (- proj1 z)) = - proj1 z.

An exact proof term for the current goal is CD_proj1_2 (conj (proj0 z)) (- proj1 z) ?? ??.

∎

End of Section CD_minus_conj_clos

Beginning of Section CD_add_clos

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Theorem. (CD_add_CD)

∀z w, CD_carr z → CD_carr w → CD_carr (z + w)

In Proofgold the corresponding term root is 7c6f64... and proposition id is ff60d4...

Proof:

Let z and w be given.

Assume Hz Hw.

We will prove CD_carr (pa (proj0 z + proj0 w) (proj1 z + proj1 w)).

Apply CD_carr_I to the current goal.

Apply F_add to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hw.

Apply F_add to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hw.

∎

Theorem. (CD_add_proj0)

∀z w, CD_carr z → CD_carr w → proj0 (z + w) = proj0 z + proj0 w

In Proofgold the corresponding term root is 76fd56... and proposition id is 258b8b...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

An exact proof term for the current goal is CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ??.

∎

Theorem. (CD_add_proj1)

∀z w, CD_carr z → CD_carr w → proj1 (z + w) = proj1 z + proj1 w

In Proofgold the corresponding term root is 1454b7... and proposition id is 2b4a1d...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

An exact proof term for the current goal is CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ??.

∎

End of Section CD_add_clos

Beginning of Section CD_mul_clos

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Theorem. (CD_mul_CD)

∀z w, CD_carr z → CD_carr w → CD_carr (z ⨯ w)

In Proofgold the corresponding term root is bda919... and proposition id is 6fa963...

Proof:

Let z and w be given.

Assume Hz Hw.

We will prove CD_carr (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w))).

Apply CD_carr_I to the current goal.

Apply F_add to the current goal.

Apply F_mul to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hw.

Apply F_minus to the current goal.

Apply F_mul to the current goal.

Apply F_conj to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hw.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

Apply F_add to the current goal.

Apply F_mul to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hw.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hz.

Apply F_mul to the current goal.

Apply CD_proj1R to the current goal.

An exact proof term for the current goal is Hz.

Apply F_conj to the current goal.

Apply CD_proj0R to the current goal.

An exact proof term for the current goal is Hw.

∎

Theorem. (CD_mul_proj0)

∀z w, CD_carr z → CD_carr w → proj0 (z ⨯ w) = proj0 z * proj0 w + - conj (proj1 w) * proj1 z

In Proofgold the corresponding term root is 7b8951... and proposition id is 411462...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

An exact proof term for the current goal is CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ??.

∎

Theorem. (CD_mul_proj1)

∀z w, CD_carr z → CD_carr w → proj1 (z ⨯ w) = proj1 w * proj0 z + proj1 z * conj (proj0 w)

In Proofgold the corresponding term root is 053f09... and proposition id is 752898...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

An exact proof term for the current goal is CD_proj1_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ??.

∎

End of Section CD_mul_clos

Beginning of Section CD_minus_conj_F

Variable minus : set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Hypothesis F_0 : F 0

Hypothesis F_minus_0 : - 0 = 0

Theorem. (CD_minus_F_eq)

∀x, F x → :-: x = - x

In Proofgold the corresponding term root is 73ac62... and proposition id is 411826...

Proof:

Let x be given.

Assume Hx.

We will prove pa (- proj0 x) (- proj1 x) = - x.

rewrite the current goal using CD_proj0_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj1_F F_0 x Hx (from left to right).

rewrite the current goal using F_minus_0 (from left to right).

We will prove pa (- x) 0 = - x.

An exact proof term for the current goal is pair_tag_0 (- x).

∎

Variable conj : set → set

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Theorem. (CD_conj_F_eq)

∀x, F x → x ' = conj x

In Proofgold the corresponding term root is a2640a... and proposition id is e715f1...

Proof:

Let x be given.

Assume Hx.

We will prove pa (conj (proj0 x)) (- proj1 x) = conj x.

rewrite the current goal using CD_proj0_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj1_F F_0 x Hx (from left to right).

rewrite the current goal using F_minus_0 (from left to right).

We will prove pa (conj x) 0 = conj x.

An exact proof term for the current goal is pair_tag_0 (conj x).

∎

End of Section CD_minus_conj_F

Beginning of Section CD_add_F

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_0 : F 0

Hypothesis F_add_0_0 : 0 + 0 = 0

Theorem. (CD_add_F_eq)

∀x y, F x → F y → x + y = x + y

In Proofgold the corresponding term root is 2e70a4... and proposition id is a784d9...

Proof:

Let x and y be given.

Assume Hx Hy.

We will prove pa (proj0 x + proj0 y) (proj1 x + proj1 y) = x + y.

rewrite the current goal using CD_proj0_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj1_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj0_F F_0 y Hy (from left to right).

rewrite the current goal using CD_proj1_F F_0 y Hy (from left to right).

rewrite the current goal using F_add_0_0 (from left to right).

We will prove pa (x + y) 0 = x + y.

An exact proof term for the current goal is pair_tag_0 (x + y).

∎

End of Section CD_add_F

Beginning of Section CD_mul_F

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_0 : F 0

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_minus_0 : - 0 = 0

Hypothesis F_add_0R : ∀x, F x → x + 0 = x

Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0

Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0

Theorem. (CD_mul_F_eq)

∀x y, F x → F y → x ⨯ y = x * y

In Proofgold the corresponding term root is 3f44c9... and proposition id is 53183f...

Proof:

Let x and y be given.

Assume Hx Hy.

We will prove pa (proj0 x * proj0 y + - conj (proj1 y) * proj1 x) (proj1 y * proj0 x + proj1 x * conj (proj0 y)) = x * y.

rewrite the current goal using CD_proj0_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj1_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj0_F F_0 y Hy (from left to right).

rewrite the current goal using CD_proj1_F F_0 y Hy (from left to right).

We will prove pa (x * y + - conj 0 * 0) (0 * x + 0 * conj y) = x * y.

rewrite the current goal using F_mul_0R (conj 0) (F_conj 0 F_0) (from left to right).

rewrite the current goal using F_mul_0L x Hx (from left to right).

rewrite the current goal using F_mul_0L (conj y) (F_conj y Hy) (from left to right).

rewrite the current goal using F_minus_0 (from left to right).

rewrite the current goal using F_add_0R 0 F_0 (from left to right).

rewrite the current goal using F_add_0R (x * y) (F_mul x y Hx Hy) (from left to right).

We will prove pa (x * y) 0 = x * y.

An exact proof term for the current goal is pair_tag_0 (x * y).

∎

End of Section CD_mul_F

Beginning of Section CD_minus_invol

Variable minus : set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_minus_invol : ∀x, F x → - - x = x

Theorem. (CD_minus_invol)

∀z, CD_carr z → :-: :-: z = z

In Proofgold the corresponding term root is 8564c2... and proposition id is 69beaf...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove pa (- proj0 (pa (- proj0 z) (- proj1 z))) (- proj1 (pa (- proj0 z) (- proj1 z))) = z.

rewrite the current goal using CD_proj0_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using F_minus_invol (proj0 z) Lp0z (from left to right).

rewrite the current goal using F_minus_invol (proj1 z) Lp1z (from left to right).

We will prove pa (proj0 z) (proj1 z) = z.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

∎

End of Section CD_minus_invol

Beginning of Section CD_conj_invol

Variable minus : set → set

Variable conj : set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_minus_invol : ∀x, F x → - - x = x

Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x

Theorem. (CD_conj_invol)

∀z, CD_carr z → z ' ' = z

In Proofgold the corresponding term root is f325ba... and proposition id is b1a97e...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove pa (conj (proj0 (pa (conj (proj0 z)) (- proj1 z)))) (- proj1 (pa (conj (proj0 z)) (- proj1 z))) = z.

rewrite the current goal using CD_proj0_2 (conj (proj0 z)) (- proj1 z) Lcp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj1_2 (conj (proj0 z)) (- proj1 z) Lcp0z Lmp1z (from left to right).

rewrite the current goal using F_conj_invol (proj0 z) Lp0z (from left to right).

rewrite the current goal using F_minus_invol (proj1 z) Lp1z (from left to right).

We will prove pa (proj0 z) (proj1 z) = z.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

∎

End of Section CD_conj_invol

Beginning of Section CD_conj_minus

Variable minus : set → set

Variable conj : set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x

Theorem. (CD_conj_minus)

∀z, CD_carr z → (:-: z) ' = :-: (z ')

In Proofgold the corresponding term root is 2e6a97... and proposition id is f23f1d...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lcmp0z: F (conj (- proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lmp0z.

We will prove pa (conj (proj0 (pa (- (proj0 z)) (- (proj1 z))))) (- proj1 (pa (- (proj0 z)) (- (proj1 z)))) = pa (- proj0 (pa (conj (proj0 z)) (- proj1 z))) (- proj1 (pa (conj (proj0 z)) (- proj1 z))).

Use f_equal.

We will prove conj (proj0 (pa (- (proj0 z)) (- (proj1 z)))) = - proj0 (pa (conj (proj0 z)) (- proj1 z)).

rewrite the current goal using CD_proj0_2 (- proj0 z) (- proj1 z) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (conj (proj0 z)) (- proj1 z) ?? ?? (from left to right).

We will prove conj (- proj0 z) = - conj (proj0 z).

An exact proof term for the current goal is F_conj_minus (proj0 z) ??.

We will prove - proj1 (pa (- (proj0 z)) (- (proj1 z))) = - proj1 (pa (conj (proj0 z)) (- proj1 z)).

Use f_equal.

rewrite the current goal using CD_proj1_2 (conj (proj0 z)) (- (proj1 z)) ?? ?? (from left to right).

An exact proof term for the current goal is CD_proj1_2 (- (proj0 z)) (- (proj1 z)) ?? ??.

∎

End of Section CD_conj_minus

Beginning of Section CD_minus_add

Variable minus : set → set

Variable add : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Theorem. (CD_minus_add)

∀z w, CD_carr z → CD_carr w → :-: (z + w) = :-: z + :-: w

In Proofgold the corresponding term root is 1b8b02... and proposition id is fb82f8...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lmp0w: F (- proj0 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0w.

We prove the intermediate claim Lmp1w: F (- proj1 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1w.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We will prove pa (- proj0 (pa (proj0 z + proj0 w) (proj1 z + proj1 w))) (- proj1 (pa (proj0 z + proj0 w) (proj1 z + proj1 w))) = pa (proj0 (pa (- proj0 z) (- proj1 z)) + proj0 (pa (- proj0 w) (- proj1 w))) (proj1 (pa (- proj0 z) (- proj1 z)) + proj1 (pa (- proj0 w) (- proj1 w))).

rewrite the current goal using CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj0_2 (- proj0 w) (- proj1 w) Lmp0w Lmp1w (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 w) (- proj1 w) Lmp0w Lmp1w (from left to right).

Use f_equal.

Apply F_minus_add to the current goal.

An exact proof term for the current goal is ??.

Apply F_minus_add to the current goal.

An exact proof term for the current goal is ??.

∎

End of Section CD_minus_add

Beginning of Section CD_conj_add

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y

Theorem. (CD_conj_add)

∀z w, CD_carr z → CD_carr w → (z + w) ' = z ' + w '

In Proofgold the corresponding term root is ac016f... and proposition id is 643b33...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0w.

We prove the intermediate claim Lmp1w: F (- proj1 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1w.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We will prove pa (conj (proj0 (pa (proj0 z + proj0 w) (proj1 z + proj1 w)))) (- proj1 (pa (proj0 z + proj0 w) (proj1 z + proj1 w))) = pa (proj0 (pa (conj (proj0 z)) (- proj1 z)) + proj0 (pa (conj (proj0 w)) (- proj1 w))) (proj1 (pa (conj (proj0 z)) (- proj1 z)) + proj1 (pa (conj (proj0 w)) (- proj1 w))).

rewrite the current goal using CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (conj (proj0 z)) (- proj1 z) Lcp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj1_2 (conj (proj0 z)) (- proj1 z) Lcp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj0_2 (conj (proj0 w)) (- proj1 w) Lcp0w Lmp1w (from left to right).

rewrite the current goal using CD_proj1_2 (conj (proj0 w)) (- proj1 w) Lcp0w Lmp1w (from left to right).

Use f_equal.

Apply F_conj_add to the current goal.

An exact proof term for the current goal is ??.

Apply F_minus_add to the current goal.

An exact proof term for the current goal is ??.

∎

End of Section CD_conj_add

Beginning of Section CD_add_com

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x

Theorem. (CD_add_com)

∀z w, CD_carr z → CD_carr w → z + w = w + z

In Proofgold the corresponding term root is bf081b... and proposition id is 5fc91f...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We will prove pa (proj0 z + proj0 w) (proj1 z + proj1 w) = pa (proj0 w + proj0 z) (proj1 w + proj1 z).

Use f_equal.

Apply F_add_com to the current goal.

An exact proof term for the current goal is ??.

Apply F_add_com to the current goal.

An exact proof term for the current goal is ??.

∎

End of Section CD_add_com

Beginning of Section CD_add_assoc

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)

Theorem. (CD_add_assoc)

∀z w u, CD_carr z → CD_carr w → CD_carr u → (z + w) + u = z + (w + u)

In Proofgold the corresponding term root is ba31a4... and proposition id is c59c2a...

Proof:

Let z, w and u be given.

Assume Hz Hw Hu.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lp0u: F (proj0 u).

An exact proof term for the current goal is CD_proj0R u Hu.

We prove the intermediate claim Lp1u: F (proj1 u).

An exact proof term for the current goal is CD_proj1R u Hu.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0wu: F (proj0 w + proj0 u).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wu: F (proj1 w + proj1 u).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

Set zw to be the term pa (proj0 z + proj0 w) (proj1 z + proj1 w).

Set wu to be the term pa (proj0 w + proj0 u) (proj1 w + proj1 u).

We will prove pa (proj0 zw + proj0 u) (proj1 zw + proj1 u) = pa (proj0 z + proj0 wu) (proj1 z + proj1 wu).

rewrite the current goal using CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 w + proj0 u) (proj1 w + proj1 u) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 w + proj0 u) (proj1 w + proj1 u) ?? ?? (from left to right).

Use f_equal.

Apply F_add_assoc to the current goal.

An exact proof term for the current goal is ??.

Apply F_add_assoc to the current goal.

An exact proof term for the current goal is ??.

∎

End of Section CD_add_assoc

Beginning of Section CD_add_0R

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_0 : F 0

Hypothesis F_add_0R : ∀x, F x → x + 0 = x

Theorem. (CD_add_0R)

∀z, CD_carr z → z + 0 = z

In Proofgold the corresponding term root is 553cb8... and proposition id is 53e78d...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We will prove pa (proj0 z + proj0 0) (proj1 z + proj1 0) = z.

rewrite the current goal using CD_proj0_F F_0 0 F_0 (from left to right).

rewrite the current goal using CD_proj1_F F_0 0 F_0 (from left to right).

rewrite the current goal using F_add_0R (proj0 z) ?? (from left to right).

rewrite the current goal using F_add_0R (proj1 z) ?? (from left to right).

We will prove pa (proj0 z) (proj1 z) = z.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

∎

End of Section CD_add_0R

Beginning of Section CD_add_0L

Variable add : set → set → set

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_0 : F 0

Hypothesis F_add_0L : ∀x, F x → 0 + x = x

Theorem. (CD_add_0L)

∀z, CD_carr z → 0 + z = z

In Proofgold the corresponding term root is d80ef4... and proposition id is 662b89...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We will prove pa (proj0 0 + proj0 z) (proj1 0 + proj1 z) = z.

rewrite the current goal using CD_proj0_F F_0 0 F_0 (from left to right).

rewrite the current goal using CD_proj1_F F_0 0 F_0 (from left to right).

rewrite the current goal using F_add_0L (proj0 z) ?? (from left to right).

rewrite the current goal using F_add_0L (proj1 z) ?? (from left to right).

We will prove pa (proj0 z) (proj1 z) = z.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

∎

End of Section CD_add_0L

Beginning of Section CD_add_minus_linv

Variable minus : set → set

Variable add : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_add_minus_linv : ∀x, F x → - x + x = 0

Theorem. (CD_add_minus_linv)

∀z, CD_carr z → :-: z + z = 0

In Proofgold the corresponding term root is 65a657... and proposition id is 477b97...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove :-: z + z = 0.

We will prove pa (proj0 (pa (- proj0 z) (- proj1 z)) + proj0 z) (proj1 (pa (- proj0 z) (- proj1 z)) + proj1 z) = 0.

rewrite the current goal using CD_proj0_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using F_add_minus_linv (proj0 z) Lp0z (from left to right).

rewrite the current goal using F_add_minus_linv (proj1 z) Lp1z (from left to right).

We will prove pa 0 0 = 0.

An exact proof term for the current goal is pair_tag_0 0.

∎

End of Section CD_add_minus_linv

Beginning of Section CD_add_minus_rinv

Variable minus : set → set

Variable add : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_add_minus_rinv : ∀x, F x → x + - x = 0

Theorem. (CD_add_minus_rinv)

∀z, CD_carr z → z + :-: z = 0

In Proofgold the corresponding term root is 6dffee... and proposition id is 7008fd...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove pa (proj0 z + proj0 (pa (- proj0 z) (- proj1 z))) (proj1 z + proj1 (pa (- proj0 z) (- proj1 z))) = 0.

rewrite the current goal using CD_proj0_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).

rewrite the current goal using F_add_minus_rinv (proj0 z) Lp0z (from left to right).

rewrite the current goal using F_add_minus_rinv (proj1 z) Lp1z (from left to right).

We will prove pa 0 0 = 0.

An exact proof term for the current goal is pair_tag_0 0.

∎

End of Section CD_add_minus_rinv

Beginning of Section CD_mul_0R

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_0 : F 0

Hypothesis F_minus_0 : - 0 = 0

Hypothesis F_conj_0 : conj 0 = 0

Hypothesis F_add_0_0 : 0 + 0 = 0

Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0

Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0

Theorem. (CD_mul_0R)

∀z, CD_carr z → z ⨯ 0 = 0

In Proofgold the corresponding term root is 9cc913... and proposition id is a15017...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We will prove pa (proj0 z * proj0 0 + - conj (proj1 0) * proj1 z) (proj1 0 * proj0 z + proj1 z * conj (proj0 0)) = 0.

rewrite the current goal using CD_proj0_F F_0 0 F_0 (from left to right).

rewrite the current goal using CD_proj1_F F_0 0 F_0 (from left to right).

We will prove pa (proj0 z * 0 + - conj 0 * proj1 z) (0 * proj0 z + proj1 z * conj 0) = 0.

rewrite the current goal using F_conj_0 (from left to right).

We will prove pa (proj0 z * 0 + - 0 * proj1 z) (0 * proj0 z + proj1 z * 0) = 0.

rewrite the current goal using F_mul_0L (proj0 z) ?? (from left to right).

rewrite the current goal using F_mul_0L (proj1 z) ?? (from left to right).

rewrite the current goal using F_mul_0R (proj0 z) ?? (from left to right).

rewrite the current goal using F_mul_0R (proj1 z) ?? (from left to right).

rewrite the current goal using F_minus_0 (from left to right).

We will prove pa (0 + 0) (0 + 0) = 0.

rewrite the current goal using F_add_0_0 (from left to right).

We will prove pa 0 0 = 0.

An exact proof term for the current goal is pair_tag_0 0.

∎

End of Section CD_mul_0R

Beginning of Section CD_mul_0L

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_0 : F 0

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_minus_0 : - 0 = 0

Hypothesis F_add_0_0 : 0 + 0 = 0

Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0

Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0

Theorem. (CD_mul_0L)

∀z, CD_carr z → 0 ⨯ z = 0

In Proofgold the corresponding term root is ab8edf... and proposition id is 31e944...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lcp1z: F (conj (proj1 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove pa (proj0 0 * proj0 z + - conj (proj1 z) * proj1 0) (proj1 z * proj0 0 + proj1 0 * conj (proj0 z)) = 0.

rewrite the current goal using CD_proj0_F F_0 0 F_0 (from left to right).

rewrite the current goal using CD_proj1_F F_0 0 F_0 (from left to right).

We will prove pa (0 * proj0 z + - conj (proj1 z) * 0) (proj1 z * 0 + 0 * conj (proj0 z)) = 0.

rewrite the current goal using F_mul_0L (proj0 z) ?? (from left to right).

rewrite the current goal using F_mul_0L (conj (proj0 z)) ?? (from left to right).

rewrite the current goal using F_mul_0R (conj (proj1 z)) ?? (from left to right).

rewrite the current goal using F_mul_0R (proj1 z) ?? (from left to right).

rewrite the current goal using F_minus_0 (from left to right).

We will prove pa (0 + 0) (0 + 0) = 0.

rewrite the current goal using F_add_0_0 (from left to right).

We will prove pa 0 0 = 0.

An exact proof term for the current goal is pair_tag_0 0.

∎

End of Section CD_mul_0L

Beginning of Section CD_mul_1R

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_0 : F 0

Hypothesis F_1 : F 1

Hypothesis F_minus_0 : - 0 = 0

Hypothesis F_conj_0 : conj 0 = 0

Hypothesis F_conj_1 : conj 1 = 1

Hypothesis F_add_0L : ∀x, F x → 0 + x = x

Hypothesis F_add_0R : ∀x, F x → x + 0 = x

Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0

Hypothesis F_mul_1R : ∀x, F x → x * 1 = x

Theorem. (CD_mul_1R)

∀z, CD_carr z → z ⨯ 1 = z

In Proofgold the corresponding term root is c55555... and proposition id is 62bb45...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We will prove pa (proj0 z * proj0 1 + - conj (proj1 1) * proj1 z) (proj1 1 * proj0 z + proj1 z * conj (proj0 1)) = z.

rewrite the current goal using CD_proj0_F F_0 1 F_1 (from left to right).

We will prove pa (proj0 z * 1 + - conj (proj1 1) * proj1 z) (proj1 1 * proj0 z + proj1 z * conj 1) = z.

rewrite the current goal using CD_proj1_F F_0 1 F_1 (from left to right).

We will prove pa (proj0 z * 1 + - conj 0 * proj1 z) (0 * proj0 z + proj1 z * conj 1) = z.

rewrite the current goal using F_conj_0 (from left to right).

rewrite the current goal using F_conj_1 (from left to right).

We will prove pa (proj0 z * 1 + - 0 * proj1 z) (0 * proj0 z + proj1 z * 1) = z.

rewrite the current goal using F_mul_1R (proj0 z) ?? (from left to right).

rewrite the current goal using F_mul_1R (proj1 z) ?? (from left to right).

rewrite the current goal using F_mul_0L (proj0 z) ?? (from left to right).

rewrite the current goal using F_mul_0L (proj1 z) ?? (from left to right).

We will prove pa (proj0 z + - 0) (0 + proj1 z) = z.

rewrite the current goal using F_minus_0 (from left to right).

We will prove pa (proj0 z + 0) (0 + proj1 z) = z.

rewrite the current goal using F_add_0L (proj1 z) ?? (from left to right).

rewrite the current goal using F_add_0R (proj0 z) ?? (from left to right).

We will prove pa (proj0 z) (proj1 z) = z.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

∎

End of Section CD_mul_1R

Beginning of Section CD_mul_1L

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_0 : F 0

Hypothesis F_1 : F 1

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_minus_0 : - 0 = 0

Hypothesis F_add_0R : ∀x, F x → x + 0 = x

Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0

Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0

Hypothesis F_mul_1L : ∀x, F x → 1 * x = x

Hypothesis F_mul_1R : ∀x, F x → x * 1 = x

Theorem. (CD_mul_1L)

∀z, CD_carr z → 1 ⨯ z = z

In Proofgold the corresponding term root is f83f52... and proposition id is 15a3f1...

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lcp1z: F (conj (proj1 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp1z.

We will prove pa (proj0 1 * proj0 z + - conj (proj1 z) * proj1 1) (proj1 z * proj0 1 + proj1 1 * conj (proj0 z)) = z.

rewrite the current goal using CD_proj0_F F_0 1 F_1 (from left to right).

rewrite the current goal using CD_proj1_F F_0 1 F_1 (from left to right).

We will prove pa (1 * proj0 z + - conj (proj1 z) * 0) (proj1 z * 1 + 0 * conj (proj0 z)) = z.

rewrite the current goal using F_mul_1L (proj0 z) ?? (from left to right).

rewrite the current goal using F_mul_1R (proj1 z) ?? (from left to right).

rewrite the current goal using F_mul_0L (conj (proj0 z)) ?? (from left to right).

rewrite the current goal using F_mul_0R (conj (proj1 z)) ?? (from left to right).

We will prove pa (proj0 z + - 0) (proj1 z + 0) = z.

rewrite the current goal using F_minus_0 (from left to right).

rewrite the current goal using F_add_0R (proj0 z) ?? (from left to right).

rewrite the current goal using F_add_0R (proj1 z) ?? (from left to right).

We will prove pa (proj0 z) (proj1 z) = z.

Use symmetry.

An exact proof term for the current goal is CD_proj0proj1_eta z Hz.

∎

End of Section CD_mul_1L

Beginning of Section CD_conj_mul

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_minus_invol : ∀x, F x → - - x = x

Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x

Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x

Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x

Hypothesis F_conj_mul : ∀x y, F x → F y → conj (x * y) = conj y * conj x

Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)

Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)

Theorem. (CD_conj_mul)

∀z w, CD_carr z → CD_carr w → (z ⨯ w) ' = w ' ⨯ z '

In Proofgold the corresponding term root is b927f8... and proposition id is 19c917...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lcp0z: F (conj (proj0 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0z.

We prove the intermediate claim Lcp1z: F (conj (proj1 z)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp1z.

We prove the intermediate claim Lmcp1z: F (- conj (proj1 z)).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lcp1z.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1z.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp0w.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is Lp1w.

We prove the intermediate claim Lmp1w: F (- proj1 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is Lp1w.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

Set w' to be the term pa (conj (proj0 w)) (- proj1 w).

Set z' to be the term pa (conj (proj0 z)) (- proj1 z).

We prove the intermediate claim Lp0w': F (proj0 w').

An exact proof term for the current goal is CD_proj0R (CD_conj minus conj w) (CD_conj_CD minus F_minus conj F_conj w Hw).

We prove the intermediate claim Lp1w': F (proj1 w').

An exact proof term for the current goal is CD_proj1R (CD_conj minus conj w) (CD_conj_CD minus F_minus conj F_conj w Hw).

We prove the intermediate claim Lp0z': F (proj0 z').

An exact proof term for the current goal is CD_proj0R (CD_conj minus conj z) (CD_conj_CD minus F_minus conj F_conj z Hz).

We prove the intermediate claim Lp1z': F (proj1 z').

An exact proof term for the current goal is CD_proj1R (CD_conj minus conj z) (CD_conj_CD minus F_minus conj F_conj z Hz).

We prove the intermediate claim Lcp0z': F (conj (proj0 z')).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1z': F (conj (proj1 z')).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0w'p0z': F (proj0 w' * proj0 z').

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1z'p1w': F (conj (proj1 z') * proj1 w').

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1z'p1w': F (- conj (proj1 z') * proj1 w').

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lw'z'L: F (proj0 w' * proj0 z' + - conj (proj1 z') * proj1 w').

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1z'p0w': F (proj1 z' * proj0 w').

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1w'cp0z': F (proj1 w' * conj (proj0 z')).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lw'z'R: F (proj1 z' * proj0 w' + proj1 w' * conj (proj0 z')).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1zp1w: F (conj (proj1 z) * proj1 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lmp1zcp0w: F ((- proj1 z) * (conj (proj0 w))).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lmp1wp0z: F ((- proj1 w) * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We will prove pa (conj (proj0 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w))))) (- (proj1 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w))))) = pa (proj0 w' * proj0 z' + - conj (proj1 z') * proj1 w') (proj1 z' * proj0 w' + proj1 w' * conj (proj0 z')).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

We will prove pa (conj (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))) = pa (proj0 w' * proj0 z' + - conj (proj1 z') * proj1 w') (proj1 z' * proj0 w' + proj1 w' * conj (proj0 z')).

rewrite the current goal using CD_proj0_2 (conj (proj0 w)) (- proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (conj (proj0 w)) (- proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (conj (proj0 z)) (- proj1 z) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (conj (proj0 z)) (- proj1 z) ?? ?? (from left to right).

We will prove pa (conj (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))) = pa (conj (proj0 w) * conj (proj0 z) + - conj (- proj1 z) * (- proj1 w)) ((- proj1 z) * (conj (proj0 w)) + (- proj1 w) * conj (conj (proj0 z))).

Use f_equal.

We will prove conj (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) = conj (proj0 w) * conj (proj0 z) + - conj (- proj1 z) * (- proj1 w).

rewrite the current goal using F_conj_add (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) ?? ?? (from left to right).

We will prove conj (proj0 z * proj0 w) + conj (- conj (proj1 w) * proj1 z) = conj (proj0 w) * conj (proj0 z) + - conj (- proj1 z) * (- proj1 w).

Use f_equal.

We will prove conj (proj0 z * proj0 w) = conj (proj0 w) * conj (proj0 z).

An exact proof term for the current goal is F_conj_mul (proj0 z) (proj0 w) ?? ??.

We will prove conj (- conj (proj1 w) * proj1 z) = - conj (- proj1 z) * (- proj1 w).

rewrite the current goal using F_conj_minus (conj (proj1 w) * proj1 z) ?? (from left to right).

Use f_equal.

We will prove conj (conj (proj1 w) * proj1 z) = conj (- proj1 z) * (- proj1 w).

rewrite the current goal using F_conj_mul (conj (proj1 w)) (proj1 z) ?? ?? (from left to right).

We will prove conj (proj1 z) * (conj (conj (proj1 w))) = conj (- proj1 z) * (- proj1 w).

rewrite the current goal using F_conj_invol (proj1 w) ?? (from left to right).

We will prove conj (proj1 z) * proj1 w = conj (- proj1 z) * (- proj1 w).

rewrite the current goal using F_conj_minus (proj1 z) ?? (from left to right).

We will prove conj (proj1 z) * proj1 w = (- conj (proj1 z)) * (- proj1 w).

rewrite the current goal using F_minus_mul_distrR (- conj (proj1 z)) (proj1 w) ?? ?? (from left to right).

rewrite the current goal using F_minus_mul_distrL (conj (proj1 z)) (proj1 w) ?? ?? (from left to right).

Use symmetry.

Apply F_minus_invol (conj (proj1 z) * proj1 w) ?? to the current goal.

We will prove - (proj1 w * proj0 z + proj1 z * conj (proj0 w)) = (- proj1 z) * (conj (proj0 w)) + (- proj1 w) * conj (conj (proj0 z)).

rewrite the current goal using F_conj_invol (proj0 z) ?? (from left to right).

rewrite the current goal using F_minus_add (proj1 w * proj0 z) (proj1 z * conj (proj0 w)) ?? ?? (from left to right).

rewrite the current goal using F_add_com ((- proj1 z) * (conj (proj0 w))) ((- proj1 w) * proj0 z) ?? ?? (from left to right).

Use f_equal.

We will prove - proj1 w * proj0 z = (- proj1 w) * proj0 z.

Use symmetry.

An exact proof term for the current goal is F_minus_mul_distrL (proj1 w) (proj0 z) ?? ??.

We will prove - proj1 z * conj (proj0 w) = (- proj1 z) * (conj (proj0 w)).

Use symmetry.

An exact proof term for the current goal is F_minus_mul_distrL (proj1 z) (conj (proj0 w)) ?? ??.

∎

End of Section CD_conj_mul

Beginning of Section CD_add_mul_distrR

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)

Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x

Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z

Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z

Theorem. (CD_add_mul_distrR)

∀z w u, CD_carr z → CD_carr w → CD_carr u → (z + w) ⨯ u = z ⨯ u + w ⨯ u

In Proofgold the corresponding term root is 3ea8d0... and proposition id is dfcffc...

Proof:

We prove the intermediate claim L_add_4_inner_mid: ∀x y z w, F x → F y → F z → F w → (x + y) + (z + w) = (x + z) + (y + w).

Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using F_add_assoc (x + y) z w (F_add x y Hx Hy) Hz Hw (from right to left).

We will prove ((x + y) + z) + w = (x + z) + (y + w).

rewrite the current goal using F_add_assoc x y z Hx Hy Hz (from left to right).

We will prove (x + (y + z)) + w = (x + z) + (y + w).

rewrite the current goal using F_add_com y z Hy Hz (from left to right).

We will prove (x + (z + y)) + w = (x + z) + (y + w).

rewrite the current goal using F_add_assoc x z y Hx Hz Hy (from right to left).

We will prove ((x + z) + y) + w = (x + z) + (y + w).

An exact proof term for the current goal is F_add_assoc (x + z) y w (F_add x z Hx Hz) Hy Hw.

Let z, w and u be given.

Assume Hz Hw Hu.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lp0u: F (proj0 u).

An exact proof term for the current goal is CD_proj0R u Hu.

We prove the intermediate claim Lp1u: F (proj1 u).

An exact proof term for the current goal is CD_proj1R u Hu.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp0u: F (conj (proj0 u)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1u: F (conj (proj1 u)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0u: F (proj0 z * proj0 u).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1z: F (conj (proj1 u) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1z: F (- conj (proj1 u) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzuL: F (proj0 z * proj0 u + - conj (proj1 u) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1up0z: F (proj1 u * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0u: F (proj1 z * conj (proj0 u)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzuR: F (proj1 u * proj0 z + proj1 z * conj (proj0 u)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0wp0u: F (proj0 w * proj0 u).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1w: F (conj (proj1 u) * proj1 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1w: F (- conj (proj1 u) * proj1 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LwuL: F (proj0 w * proj0 u + - conj (proj1 u) * proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1up0w: F (proj1 u * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wcp0u: F (proj1 w * conj (proj0 u)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LwuR: F (proj1 u * proj0 w + proj1 w * conj (proj0 u)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

Set zw to be the term pa (proj0 z + proj0 w) (proj1 z + proj1 w).

Set zu to be the term pa (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)).

Set wu to be the term pa (proj0 w * proj0 u + - conj (proj1 u) * proj1 w) (proj1 u * proj0 w + proj1 w * conj (proj0 u)).

We will prove pa (proj0 zw * proj0 u + - conj (proj1 u) * proj1 zw) (proj1 u * proj0 zw + proj1 zw * conj (proj0 u)) = pa (proj0 zu + proj0 wu) (proj1 zu + proj1 wu).

rewrite the current goal using CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

We will prove pa ((proj0 z + proj0 w) * proj0 u + - conj (proj1 u) * (proj1 z + proj1 w)) (proj1 u * (proj0 z + proj0 w) + (proj1 z + proj1 w) * conj (proj0 u)) = pa (proj0 zu + proj0 wu) (proj1 zu + proj1 wu).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 w * proj0 u + - conj (proj1 u) * proj1 w) (proj1 u * proj0 w + proj1 w * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 w * proj0 u + - conj (proj1 u) * proj1 w) (proj1 u * proj0 w + proj1 w * conj (proj0 u)) ?? ?? (from left to right).

Use f_equal.

We will prove (proj0 z + proj0 w) * proj0 u + - conj (proj1 u) * (proj1 z + proj1 w) = (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) + (proj0 w * proj0 u + - conj (proj1 u) * proj1 w).

rewrite the current goal using L_add_4_inner_mid (proj0 z * proj0 u) (- conj (proj1 u) * proj1 z) (proj0 w * proj0 u) (- conj (proj1 u) * proj1 w) ?? ?? ?? ?? (from left to right).

Use f_equal.

We will prove (proj0 z + proj0 w) * proj0 u = proj0 z * proj0 u + proj0 w * proj0 u.

Apply F_add_mul_distrR to the current goal.

An exact proof term for the current goal is ??.

We will prove - conj (proj1 u) * (proj1 z + proj1 w) = (- conj (proj1 u) * proj1 z) + (- conj (proj1 u) * proj1 w).

rewrite the current goal using F_minus_add (conj (proj1 u) * proj1 z) (conj (proj1 u) * proj1 w) ?? ?? (from right to left).

Use f_equal.

We will prove conj (proj1 u) * (proj1 z + proj1 w) = (conj (proj1 u) * proj1 z) + (conj (proj1 u) * proj1 w).

Apply F_add_mul_distrL to the current goal.

An exact proof term for the current goal is ??.

We will prove (proj1 u * (proj0 z + proj0 w) + (proj1 z + proj1 w) * conj (proj0 u)) = (proj1 u * proj0 z + proj1 z * conj (proj0 u)) + (proj1 u * proj0 w + proj1 w * conj (proj0 u)).

rewrite the current goal using L_add_4_inner_mid (proj1 u * proj0 z) (proj1 z * conj (proj0 u)) (proj1 u * proj0 w) (proj1 w * conj (proj0 u)) ?? ?? ?? ?? (from left to right).

Use f_equal.

Apply F_add_mul_distrL to the current goal.

An exact proof term for the current goal is ??.

Apply F_add_mul_distrR to the current goal.

An exact proof term for the current goal is ??.

∎

End of Section CD_add_mul_distrR

Beginning of Section CD_add_mul_distrL

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y

Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)

Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x

Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z

Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z

Theorem. (CD_add_mul_distrL)

∀z w u, CD_carr z → CD_carr w → CD_carr u → z ⨯ (w + u) = z ⨯ w + z ⨯ u

In Proofgold the corresponding term root is 45d05f... and proposition id is 447dab...

Proof:

We prove the intermediate claim L_add_4_inner_mid: ∀x y z w, F x → F y → F z → F w → (x + y) + (z + w) = (x + z) + (y + w).

Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using F_add_assoc (x + y) z w (F_add x y Hx Hy) Hz Hw (from right to left).

We will prove ((x + y) + z) + w = (x + z) + (y + w).

rewrite the current goal using F_add_assoc x y z Hx Hy Hz (from left to right).

We will prove (x + (y + z)) + w = (x + z) + (y + w).

rewrite the current goal using F_add_com y z Hy Hz (from left to right).

We will prove (x + (z + y)) + w = (x + z) + (y + w).

rewrite the current goal using F_add_assoc x z y Hx Hz Hy (from right to left).

We will prove ((x + z) + y) + w = (x + z) + (y + w).

An exact proof term for the current goal is F_add_assoc (x + z) y w (F_add x z Hx Hz) Hy Hw.

Let z, w and u be given.

Assume Hz Hw Hu.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lp0u: F (proj0 u).

An exact proof term for the current goal is CD_proj0R u Hu.

We prove the intermediate claim Lp1u: F (proj1 u).

An exact proof term for the current goal is CD_proj1R u Hu.

We prove the intermediate claim Lp0wu: F (proj0 w + proj0 u).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wu: F (proj1 w + proj1 u).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp0u: F (conj (proj0 u)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1u: F (conj (proj1 u)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzwR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0u: F (proj0 z * proj0 u).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1z: F (conj (proj1 u) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1z: F (- conj (proj1 u) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzuL: F (proj0 z * proj0 u + - conj (proj1 u) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1up0z: F (proj1 u * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0u: F (proj1 z * conj (proj0 u)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzuR: F (proj1 u * proj0 z + proj1 z * conj (proj0 u)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

Set wu to be the term pa (proj0 w + proj0 u) (proj1 w + proj1 u).

Set zw to be the term pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Set zu to be the term pa (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)).

We will prove pa (proj0 z * proj0 wu + - conj (proj1 wu) * proj1 z) (proj1 wu * proj0 z + proj1 z * conj (proj0 wu)) = pa (proj0 zw + proj0 zu) (proj1 zw + proj1 zu).

rewrite the current goal using CD_proj0_2 (proj0 w + proj0 u) (proj1 w + proj1 u) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 w + proj0 u) (proj1 w + proj1 u) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)) ?? ?? (from left to right).

Use f_equal.

rewrite the current goal using L_add_4_inner_mid (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) (proj0 z * proj0 u) (- conj (proj1 u) * proj1 z) ?? ?? ?? ?? (from left to right).

Use f_equal.

Apply F_add_mul_distrL to the current goal.

An exact proof term for the current goal is ??.

We will prove - conj (proj1 w + proj1 u) * proj1 z = (- conj (proj1 w) * proj1 z) + (- conj (proj1 u) * proj1 z).

rewrite the current goal using F_conj_add (proj1 w) (proj1 u) ?? ?? (from left to right).

We will prove - (conj (proj1 w) + conj (proj1 u)) * proj1 z = (- conj (proj1 w) * proj1 z) + (- conj (proj1 u) * proj1 z).

rewrite the current goal using F_add_mul_distrR (conj (proj1 w)) (conj (proj1 u)) (proj1 z) ?? ?? ?? (from left to right).

We will prove - (conj (proj1 w) * proj1 z + conj (proj1 u) * proj1 z) = (- conj (proj1 w) * proj1 z) + (- conj (proj1 u) * proj1 z).

Apply F_minus_add to the current goal.

An exact proof term for the current goal is ??.

rewrite the current goal using L_add_4_inner_mid (proj1 w * proj0 z) (proj1 z * conj (proj0 w)) (proj1 u * proj0 z) (proj1 z * conj (proj0 u)) ?? ?? ?? ?? (from left to right).

Use f_equal.

Apply F_add_mul_distrR to the current goal.

An exact proof term for the current goal is ??.

We will prove proj1 z * conj (proj0 w + proj0 u) = proj1 z * conj (proj0 w) + proj1 z * conj (proj0 u).

rewrite the current goal using F_conj_add (proj0 w) (proj0 u) ?? ?? (from left to right).

Apply F_add_mul_distrL to the current goal.

An exact proof term for the current goal is ??.

∎

End of Section CD_add_mul_distrL

Beginning of Section CD_minus_mul_distrR

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)

Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)

Theorem. (CD_minus_mul_distrR)

∀z w, CD_carr z → CD_carr w → z ⨯ (:-: w) = :-: z ⨯ w

In Proofgold the corresponding term root is 92051e... and proposition id is 34f645...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lmp0w: F (- proj0 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lmp1w: F (- proj1 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lmcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LmulL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LmulR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We will prove pa (proj0 z * proj0 (pa (- proj0 w) (- proj1 w)) + - conj (proj1 (pa (- proj0 w) (- proj1 w))) * proj1 z) (proj1 (pa (- proj0 w) (- proj1 w)) * proj0 z + proj1 z * conj (proj0 (pa (- proj0 w) (- proj1 w)))) = pa (- proj0 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)))) (- proj1 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)))).

rewrite the current goal using CD_proj0_2 (- proj0 w) (- proj1 w) (F_minus (proj0 w) (CD_proj0R w Hw)) ?? (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 w) (- proj1 w) (F_minus (proj0 w) (CD_proj0R w Hw)) ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

We will prove pa (proj0 z * (- proj0 w) + - conj (- proj1 w) * proj1 z) ((- proj1 w) * proj0 z + proj1 z * conj (- proj0 w)) = pa (- (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))).

Use f_equal.

We will prove proj0 z * (- proj0 w) + - conj (- proj1 w) * proj1 z = - (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

rewrite the current goal using F_minus_add (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) ?? ?? (from left to right).

Use f_equal.

We will prove proj0 z * (- proj0 w) = - proj0 z * proj0 w.

An exact proof term for the current goal is F_minus_mul_distrR (proj0 z) (proj0 w) ?? ??.

We will prove - conj (- proj1 w) * proj1 z = - - conj (proj1 w) * proj1 z.

Use f_equal.

We will prove conj (- proj1 w) * proj1 z = - conj (proj1 w) * proj1 z.

rewrite the current goal using F_conj_minus (proj1 w) ?? (from left to right).

An exact proof term for the current goal is F_minus_mul_distrL (conj (proj1 w)) (proj1 z) ?? ??.

We will prove (- proj1 w) * proj0 z + proj1 z * conj (- proj0 w) = - (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

rewrite the current goal using F_minus_add (proj1 w * proj0 z) (proj1 z * conj (proj0 w)) ?? ?? (from left to right).

Use f_equal.

We will prove (- proj1 w) * proj0 z = - proj1 w * proj0 z.

An exact proof term for the current goal is F_minus_mul_distrL (proj1 w) (proj0 z) ?? ??.

We will prove proj1 z * conj (- proj0 w) = - proj1 z * conj (proj0 w).

rewrite the current goal using F_conj_minus (proj0 w) ?? (from left to right).

An exact proof term for the current goal is F_minus_mul_distrR (proj1 z) (conj (proj0 w)) ?? ??.

∎

End of Section CD_minus_mul_distrR

Beginning of Section CD_minus_mul_distrL

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y

Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)

Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)

Theorem. (CD_minus_mul_distrL)

∀z w, CD_carr z → CD_carr w → (:-: z) ⨯ w = :-: z ⨯ w

In Proofgold the corresponding term root is 8f6dad... and proposition id is bd692d...

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lmp0z: F (- proj0 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lmp1z: F (- proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp0w: F (conj (proj0 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1w: F (conj (proj1 w)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lmcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LmulL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LmulR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We will prove pa (proj0 (pa (- proj0 z) (- proj1 z)) * proj0 w + - conj (proj1 w) * proj1 (pa (- proj0 z) (- proj1 z))) (proj1 w * proj0 (pa (- proj0 z) (- proj1 z)) + proj1 (pa (- proj0 z) (- proj1 z)) * conj (proj0 w)) = pa (- proj0 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)))) (- proj1 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)))).

rewrite the current goal using CD_proj0_2 (- proj0 z) (- proj1 z) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (- proj0 z) (- proj1 z) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).

We will prove pa ((- proj0 z) * proj0 w + - conj (proj1 w) * (- proj1 z)) (proj1 w * (- proj0 z) + (- proj1 z) * conj (proj0 w)) = pa (- (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))).

Use f_equal.

We will prove (- proj0 z) * proj0 w + - conj (proj1 w) * (- proj1 z) = - (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).

rewrite the current goal using F_minus_add (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) ?? ?? (from left to right).

Use f_equal.

We will prove (- proj0 z) * proj0 w = - proj0 z * proj0 w.

An exact proof term for the current goal is F_minus_mul_distrL (proj0 z) (proj0 w) ?? ??.

We will prove - conj (proj1 w) * (- proj1 z) = - - conj (proj1 w) * proj1 z.

Use f_equal.

We will prove conj (proj1 w) * (- proj1 z) = - conj (proj1 w) * proj1 z.

An exact proof term for the current goal is F_minus_mul_distrR (conj (proj1 w)) (proj1 z) ?? ??.

We will prove proj1 w * (- proj0 z) + (- proj1 z) * conj (proj0 w) = - (proj1 w * proj0 z + proj1 z * conj (proj0 w)).

rewrite the current goal using F_minus_add (proj1 w * proj0 z) (proj1 z * conj (proj0 w)) ?? ?? (from left to right).

Use f_equal.

We will prove proj1 w * (- proj0 z) = - proj1 w * proj0 z.

An exact proof term for the current goal is F_minus_mul_distrR (proj1 w) (proj0 z) ?? ??.

We will prove (- proj1 z) * conj (proj0 w) = - proj1 z * conj (proj0 w).

An exact proof term for the current goal is F_minus_mul_distrL (proj1 z) (conj (proj0 w)) ?? ??.

∎

End of Section CD_minus_mul_distrL

Beginning of Section CD_exp_nat

Variable minus : set → set

Variable conj : set → set

Variable add : set → set → set

Variable mul : set → set → set

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul.

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term CD_minus minus.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term CD_add add.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term CD_mul minus conj add mul.

Notation. We use ^ as an infix operator with priority 342 and no associativity corresponding to applying term CD_exp_nat minus conj add mul.

Theorem. (CD_exp_nat_0)

∀z, z ^ 0 = 1

In Proofgold the corresponding term root is f63bba... and proposition id is 2c1506...

Proof:

Let z be given.

An exact proof term for the current goal is nat_primrec_0 1 (λ_ r ⇒ z ⨯ r).

∎

Theorem. (CD_exp_nat_S)

∀z n, nat_p n → z ^ (ordsucc n) = z ⨯ z ^ n

In Proofgold the corresponding term root is 56eeed... and proposition id is 5b5f54...

Proof:

Let z and n be given.

Assume Hn.

An exact proof term for the current goal is nat_primrec_S 1 (λ_ r ⇒ z ⨯ r) n Hn.

∎

Beginning of Section CD_exp_nat_1_2

Hypothesis F_0 : F 0

Hypothesis F_1 : F 1

Hypothesis F_minus_0 : - 0 = 0

Hypothesis F_conj_0 : conj 0 = 0

Hypothesis F_conj_1 : conj 1 = 1

Hypothesis F_add_0L : ∀x, F x → 0 + x = x

Hypothesis F_add_0R : ∀x, F x → x + 0 = x

Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0

Hypothesis F_mul_1R : ∀x, F x → x * 1 = x

Theorem. (CD_exp_nat_1)

∀z, CD_carr z → z ^ 1 = z

In Proofgold the corresponding term root is cbb149... and proposition id is e01fe9...

Proof:

Let z be given.

Assume Hz.

rewrite the current goal using CD_exp_nat_S z 0 nat_0 (from left to right).

We will prove z ⨯ z ^ 0 = z.

rewrite the current goal using CD_exp_nat_0 z (from left to right).

We will prove z ⨯ 1 = z.

An exact proof term for the current goal is CD_mul_1R minus conj add mul F_0 F_1 F_minus_0 F_conj_0 F_conj_1 F_add_0L F_add_0R F_mul_0L F_mul_1R z Hz.

∎

Theorem. (CD_exp_nat_2)

∀z, CD_carr z → z ^ 2 = z ⨯ z

In Proofgold the corresponding term root is c5241d... and proposition id is 9b74d2...

Proof:

Let z be given.

Assume Hz.

rewrite the current goal using CD_exp_nat_S z 1 nat_1 (from left to right).

We will prove z ⨯ z ^ 1 = z ⨯ z.

Use f_equal.

An exact proof term for the current goal is CD_exp_nat_1 z Hz.

∎

End of Section CD_exp_nat_1_2

Hypothesis F_minus : ∀x, F x → F (- x)

Hypothesis F_conj : ∀x, F x → F (conj x)

Hypothesis F_add : ∀x y, F x → F y → F (x + y)

Hypothesis F_mul : ∀x y, F x → F y → F (x * y)

Hypothesis F_0 : F 0

Hypothesis F_1 : F 1

Theorem. (CD_exp_nat_CD)

∀z, CD_carr z → ∀n, nat_p n → CD_carr (z ^ n)

In Proofgold the corresponding term root is 43212b... and proposition id is a1e10b...

Proof:

Let z be given.

Assume Hz.

Apply nat_ind to the current goal.

rewrite the current goal using CD_exp_nat_0 (from left to right).

We will prove CD_carr 1.

An exact proof term for the current goal is CD_carr_0ext F_0 1 F_1.

Let n be given.

Assume Hn.

Assume IHn: CD_carr (z ^ n).

rewrite the current goal using CD_exp_nat_S z n Hn (from left to right).

We will prove CD_carr (z ⨯ z ^ n).

Apply CD_mul_CD minus conj add mul F_minus F_conj F_add F_mul to the current goal.

We will prove CD_carr z.

An exact proof term for the current goal is Hz.

We will prove CD_carr (z ^ n).

An exact proof term for the current goal is IHn.

∎

End of Section CD_exp_nat

End of Section Alg