Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_ind with λ x0 . ∀ x1 . equip x1 x0 ⟶ equip (prim4 x1) (exp_SNo_nat 2 x0) leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: equip x0 0.
Apply equip_0_Empty with x0, λ x1 x2 . equip (prim4 x2) (exp_SNo_nat 2 0) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply exp_SNo_nat_0 with 2, λ x1 x2 . equip (prim4 0) x2 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply Power_0_Sing_0 with λ x1 x2 . equip x2 1.
Apply eq_1_Sing0 with λ x1 x2 . equip x1 1.
The subproof is completed by applying equip_ref with 1.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . equip x1 x0 ⟶ equip (prim4 x1) (exp_SNo_nat 2 x0).
Let x1 of type ι be given.
Assume H2: equip x1 (ordsucc x0).
Apply exp_SNo_nat_S with 2, x0, λ x2 x3 . equip (prim4 x1) x3 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
Apply add_SNo_1_1_2 with λ x2 x3 . equip (prim4 x1) (mul_SNo x2 (exp_SNo_nat 2 x0)).
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Apply mul_SNo_distrR with 1, 1, exp_SNo_nat 2 x0, λ x2 x3 . equip (prim4 x1) x3 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L6.
Apply mul_SNo_oneL with exp_SNo_nat 2 x0, λ x2 x3 . equip (prim4 x1) (add_SNo x3 x3) leaving 2 subgoals.
The subproof is completed by applying L6.
Apply equip_sym with x1, ordsucc x0, ∃ x2 . x2 ∈ x1, equip (prim4 x1) (add_SNo (exp_SNo_nat 2 x0) (exp_SNo_nat 2 x0)) leaving 3 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι → ι be given.
Assume H9: bij (ordsucc x0) x1 x2.
Apply H9 with ∃ x3 . x3 ∈ x1.
Assume H10: and (∀ x3 . x3 ∈ ordsucc x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ ordsucc x0 ⟶ ∀ x4 . x4 ∈ ordsucc x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4).
Assume H11: ∀ x3 . x3 ∈ x1 ⟶ ∃ x4 . and (x4 ∈ ordsucc x0) (x2 x4 = x3).
Apply H10 with ∃ x3 . x3 ∈ x1.
Assume H12: ∀ x3 . x3 ∈ ordsucc x0 ⟶ x2 x3 ∈ x1.
Assume H13: ∀ x3 . x3 ∈ ordsucc x0 ⟶ ∀ x4 . x4 ∈ ordsucc x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Let x3 of type ο be given.
Assume H14: ∀ x4 . x4 ∈ x1 ⟶ x3.
Apply H14 with x2 x0.
Apply H12 with x0.
The subproof is completed by applying ordsuccI2 with x0.
Let x2 of type ι be given.
Assume H9: (λ x3 . x3 ∈ x1) x2.
Apply H1 with setminus x1 (Sing x2), equip (prim4 x1) (add_SNo (exp_SNo_nat 2 x0) (exp_SNo_nat 2 x0)) leaving 2 subgoals.
Apply unknownprop_997b324045b1165b0cf38788927ff324ddb3a505c8b91e290586e4dd5480f2bd with x1, x0, x2 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H2.
Let x3 of type ι → ι be given.
Assume H10: bij (prim4 (setminus x1 (Sing x2))) (exp_SNo_nat 2 x0) x3.
Apply H10 with equip (prim4 x1) (add_SNo (exp_SNo_nat 2 x0) (exp_SNo_nat 2 x0)).
Assume H11: and (∀ x4 . ... ∈ ... ⟶ x3 x4 ∈ exp_SNo_nat 2 x0) ....
...
■