Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: ∃ x1 . x0 x1.
Apply dneg with x0 (prim0 ((λ x1 : ι → ο . Descr_Vo1 (λ x2 : ι → ο . and ((λ x3 : ι → ο . ∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x4 ((λ x6 : ι → ο . λ x7 . and (x6 x7) (x7 = prim0 (λ x8 . x6 x8) ⟶ ∀ x8 : ο . x8)) x5)) ⟶ (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x4 x6) ⟶ x4 (Descr_Vo1 x5)) ⟶ x4 x3) x2) (∀ x3 . x1 x3 ⟶ x2 x3))) x0)).
Assume H1: not (x0 (prim0 ((λ x1 : ι → ο . Descr_Vo1 (λ x2 : ι → ο . and ((λ x3 : ι → ο . ∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x4 ((λ x6 : ι → ο . λ x7 . and (x6 x7) (x7 = prim0 (λ x8 . x6 x8) ⟶ ∀ x8 : ο . x8)) x5)) ⟶ (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x4 x6) ⟶ x4 (Descr_Vo1 x5)) ⟶ x4 x3) x2) (∀ x3 . x1 x3 ⟶ x2 x3))) x0))).
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: (λ x1 : ι → ο . Descr_Vo1 (λ x2 : ι → ο . and ((λ x3 : ι → ο . ∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x4 ((λ x6 : ι → ο . λ x7 . and (x6 x7) (x7 = prim0 (λ x8 . x6 x8) ⟶ ∀ x8 : ο . x8)) x5)) ⟶ (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x4 x6) ⟶ x4 (Descr_Vo1 x5)) ⟶ x4 x3) x2) (∀ x3 . x1 x3 ⟶ x2 x3))) x0 (prim0 ((λ x1 : ι → ο . Descr_Vo1 (λ x2 : ι → ο . and ((λ x3 : ι → ο . ∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x4 ((λ x6 : ι → ο . λ x7 . and (x6 x7) (x7 = prim0 (λ x8 . x6 x8) ⟶ ∀ x8 : ο . x8)) x5)) ⟶ (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x4 x6) ⟶ x4 (Descr_Vo1 x5)) ⟶ x4 x3) x2) (∀ x3 . x1 x3 ⟶ x2 x3))) x0))
Apply Eps_i_ex with (λ x1 : ι → ο . Descr_Vo1 (λ x2 : ι → ο . and ((λ x3 : ι → ο . ∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . ... ⟶ x4 ((λ x6 : ι → ο . λ x7 . and (x6 x7) (x7 = prim0 (λ x8 . x6 x8) ⟶ ∀ x8 : ο . x8)) ...)) ⟶ (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x4 x6) ⟶ x4 (Descr_Vo1 x5)) ⟶ x4 x3) ...) ...)) ....
...
Apply L2.
Apply L5 with prim0 ((λ x1 : ι → ο . Descr_Vo1 (λ x2 : ι → ο . and ((λ x3 : ι → ο . ∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x4 ((λ x6 : ι → ο . λ x7 . and (x6 x7) (x7 = prim0 (λ x8 . x6 x8) ⟶ ∀ x8 : ο . x8)) x5)) ⟶ (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x4 x6) ⟶ x4 (Descr_Vo1 x5)) ⟶ x4 x3) x2) (∀ x3 . x1 x3 ⟶ x2 x3))) x0).
The subproof is completed by applying L7.
■