Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: HSNo x0.
Assume H1: HSNo x1.
Assume H2: HSNo x2.
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
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: ...
...
Claim L51: ...
...
Claim L52: ...
...
Claim L53: ...
...
Claim L54: ...
...
Claim L55: ...
...
Claim L56: ...
...
Claim L57: ...
...
Claim L58: ...
...
Claim L59: ...
...
Claim L60: ...
...
Claim L61: ...
...
Claim L62: ...
...
Claim L63: ...
...
Claim L64: ...
...
Claim L65: ...
...
Claim L66: ...
...
Claim L67: ...
...
Claim L68: ...
...
Claim L69: ...
...
Claim L70: ...
...
Claim L71: ...
...
Claim L72: ...
...
Claim L73: ...
...
Claim L74: ...
...
Claim L75: ...
...
Claim L76: ...
...
Claim L77: ...
...
Claim L78: ...
...
Claim L79: ...
...
Claim L80: ...
...
Claim L81: ...
...
Claim L82: ...
...
Claim L83: ...
...
Claim L84: ...
...
Claim L85: ...
...
Claim L86: ...
...
Claim L87: ...
...
Claim L88: ...
...
Claim L89: ...
...
Claim L90: ...
...
Claim L91: ...
...
Claim L92: ...
...
Claim L93: ...
...
Claim L94: ...
...
Claim L95: ...
...
Claim L96: ...
...
Claim L97: ...
...
Claim L98: ...
...
Claim L99: ...
...
Claim L100: ...
...
Claim L101: ...
...
Claim L102: ...
...
Apply HSNo_proj0proj1_split with mul_HSNo x0 (mul_HSNo x1 x2), mul_HSNo (mul_HSNo x0 x1) x2 leaving 4 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
set y3 to be ...
set y4 to be ...
Claim L103: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Assume H103: x5 (HSNo_proj0 (mul_HSNo (mul_HSNo x2 y3) y4)).
Apply mul_HSNo_proj0 with x2, mul_HSNo y3 y4, λ x6 . x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y6 to be ...
set y7 to be ...
Claim L104: ...
...
set y8 to be ...
Apply L104 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H105: y8 y7 y7.
The subproof is completed by applying H105.
Apply add_CSNo_assoc with mul_CSNo (HSNo_proj0 x5) (mul_CSNo (HSNo_proj0 y6) (HSNo_proj0 y7)), minus_CSNo (mul_CSNo (HSNo_proj0 x5) (mul_CSNo (conj_CSNo (HSNo_proj1 y7)) (HSNo_proj1 y6))), add_CSNo (minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj0 y6)) (mul_CSNo (conj_CSNo (HSNo_proj1 y7)) (HSNo_proj1 x5)))) (minus_CSNo (mul_CSNo (HSNo_proj0 y7) (mul_CSNo (conj_CSNo (HSNo_proj1 y6)) (HSNo_proj1 x5)))), λ x9 x10 . add_CSNo (mul_CSNo (HSNo_proj0 x5) (add_CSNo (mul_CSNo (HSNo_proj0 y6) (HSNo_proj0 y7)) (minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj1 y7)) (HSNo_proj1 y6))))) (minus_CSNo (mul_CSNo (conj_CSNo (add_CSNo (mul_CSNo (HSNo_proj1 y7) (HSNo_proj0 y6)) (mul_CSNo (HSNo_proj1 y6) (conj_CSNo (HSNo_proj0 y7))))) (HSNo_proj1 x5))) = x9, λ x9 . y8 leaving 5 subgoals.
The subproof is completed by applying L47.
The subproof is completed by applying L59.
The subproof is completed by applying L82.
set y9 to be ...
set y10 to be ...
Claim L105: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
Assume H105: x11 (add_CSNo (add_CSNo (mul_CSNo (HSNo_proj0 y7) (mul_CSNo (HSNo_proj0 y8) (HSNo_proj0 y9))) (minus_CSNo (mul_CSNo (HSNo_proj0 y7) (mul_CSNo (conj_CSNo (HSNo_proj1 y9)) (HSNo_proj1 y8))))) (add_CSNo (minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj0 y8)) (mul_CSNo (conj_CSNo (HSNo_proj1 y9)) (HSNo_proj1 y7)))) (minus_CSNo (mul_CSNo (HSNo_proj0 y9) (mul_CSNo (conj_CSNo (HSNo_proj1 y8)) (HSNo_proj1 y7)))))).
set y12 to be ...
Apply mul_CSNo_distrL with HSNo_proj0 y7, mul_CSNo (HSNo_proj0 y8) (HSNo_proj0 y9), minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj1 y9)) (HSNo_proj1 y8)), λ x13 x14 . x14 = add_CSNo (mul_CSNo (HSNo_proj0 y7) (mul_CSNo (HSNo_proj0 y8) (HSNo_proj0 y9))) (minus_CSNo (mul_CSNo (HSNo_proj0 y7) (mul_CSNo (conj_CSNo (HSNo_proj1 y9)) (HSNo_proj1 y8)))), λ x13 x14 . y12 (add_CSNo x13 (minus_CSNo (mul_CSNo (conj_CSNo (add_CSNo (mul_CSNo (HSNo_proj1 y9) (HSNo_proj0 y8)) (mul_CSNo ... ...))) ...))) ... leaving 5 subgoals.
...
...
...
...
...
Let x11 of type ι → ι → ο be given.
Apply L105 with λ x12 . x11 x12 y10 ⟶ x11 y10 x12.
Assume H106: x11 y10 y10.
The subproof is completed by applying H106.
...
Let x5 of type ι → ι → ο be given.
Apply L103 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H104: x5 y4 y4.
The subproof is completed by applying H104.
...
■