Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u17.
Assume H1: atleastp u5 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u18).
Assume H3: ∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u20).
Assume H4: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2).
Claim L5: ...
...
Apply unknownprop_500d1e737e2209e4c583d05afc878803ba55ca9b82cd3357b41edde686af0c3b with u4, x0, False leaving 4 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying H1.
The subproof is completed by applying L5.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H6: equip u4 x1.
Assume H7: x2 ∈ x0.
Assume H8: x1 ⊆ x0.
Assume H9: x1 ⊆ x2.
Claim L10: ...
...
Apply unknownprop_9c3c4976195baf6bd37497317b74ca268d712dfbd75862a7bcb0572a39ded839 with u3, x1, False leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H11: x3 ∈ x1.
Apply L5 with x3.
Apply H8 with x3.
The subproof is completed by applying H11.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H11: equip u3 x3.
Assume H12: x4 ∈ x1.
Assume H13: x3 ⊆ x1.
Assume H14: x3 ⊆ x4.
Assume H15: x1 = binunion x3 (Sing x4).
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Apply unknownprop_5a83a108ad757ace387d2c518b5833379f1ee4db5a9903e44819e140b2ab80ec with x3, False leaving 3 subgoals.
Apply equip_atleastp with u3, x3.
The subproof is completed by applying H11.
Let x5 of type ι be given.
Assume H20: x5 ∈ x3.
Apply L5 with x5.
Apply H8 with x5.
Apply H13 with x5.
The subproof is completed by applying H20.
Let x5 of type ι be given.
Assume H20: x5 ∈ x3.
Let x6 of type ι be given.
Assume H21: x6 ∈ x3.
Let x7 of type ι be given.
Assume H22: x7 ∈ x3.
Assume H23: x5 ∈ x6.
Assume H24: x6 ∈ x7.
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Claim L37: ...
...
Claim L38: ...
...
Claim L39: ...
...
Claim L40: ...
...
Claim L41: ...
...
Claim L42: ...
...
Claim L43: ...
...
Claim L44: ...
...
Claim L45: ...
...
Claim L46: ...
...
Claim L47: ...
...
Claim L48: ...
...
Claim L49: ...
...
Claim L50: ...
...
Apply unknownprop_d2eb1da8f945e97882f3b17888a7fe6e441c3a4b20ad156ba00c22e721803915 with x2, λ x8 . x2 = x8 ⟶ ∀ x9 : ο . x9 leaving 7 subgoals.
Apply setminusI with u17, u12, x2 leaving 2 subgoals.
Apply H0 with x2.
The subproof is completed by applying H7.
Assume H51: x2 ∈ u12.
Claim L52: binunion x1 (Sing x2) ⊆ u12
Let x8 of type ι be given.
Assume H52: x8 ∈ binunion x1 (Sing x2).
Apply binunionE with x1, Sing x2, x8, x8 ∈ u12 leaving 3 subgoals.
The subproof is completed by applying H52.
Assume H53: x8 ∈ x1.
Apply nat_trans with u12, x2, x8 leaving 3 subgoals.
The subproof is completed by applying nat_12.
...
...
...
Apply unknownprop_82a4043338dce48d58934c215ccdbe85be545db6869ac125d5e92b153cac28bb with binunion x1 (Sing x2) leaving 3 subgoals.
The subproof is completed by applying L52.
Apply equip_atleastp with u5, binunion x1 (Sing x2).
Apply equip_tra with u5, setsum x1 (Sing x2), binunion x1 (Sing x2) leaving 2 subgoals.
Apply unknownprop_150e303ecf8a7227a9f23528d11666f9ad495de0a25ae8fba20dedf2c3db2f83 with λ x8 x9 . equip x8 (setsum x1 (Sing x2)).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with u4, u1, x1, Sing x2 leaving 4 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying nat_1.
The subproof is completed by applying H6.
Apply equip_sym with Sing x2, u1.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x2.
Apply equip_sym with binunion x1 (Sing x2), setsum x1 (Sing x2).
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with x1, Sing x2, x1, Sing x2 leaving 3 subgoals.
The subproof is completed by applying equip_ref with x1.
The subproof is completed by applying equip_ref with Sing x2.
Let x8 of type ι be given.
Assume H53: x8 ∈ x1.
Assume H54: x8 ∈ Sing x2.
Apply In_irref with x2.
Apply SingE with x2, x8, λ x9 x10 . x9 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H54.
Apply H9 with x8.
The subproof is completed by applying H53.
Let x8 of type ι be given.
Assume H53: x8 ∈ binunion x1 (Sing x2).
Let x9 of type ι be given.
Assume H54: x9 ∈ binunion x1 (Sing x2).
Assume H55: x8 = x9 ⟶ ∀ x10 : ο . x10.
Assume H56: TwoRamseyGraph_3_6_17 x8 x9.
Apply H4 with x8, x9 leaving 4 subgoals.
Apply L10 with x8.
The subproof is completed by applying H53.
Apply L10 with x9.
The subproof is completed by applying H54.
The subproof is completed by applying H55.
Apply unknownprop_331d7f66eeb37dc381bf2e3606d3b3c601f9b8768b689e8985564581b76a5fdc with x8, x9 leaving 3 subgoals.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with x8.
Apply L52 with x8.
The subproof is completed by applying H53.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with x9.
Apply L52 with x9.
The subproof is completed by applying H54.
The subproof is completed by applying H56.
...
...
...
...
...
...
■