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.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Let x13 of type ι be given.
Let x14 of type ι be given.
Let x15 of type ι be given.
Let x16 of type ι be given.
Let x17 of type ι be given.
Let x18 of type ι be given.
Let x19 of type ι be given.
Let x20 of type ι be given.
Let x21 of type ι be given.
Let x22 of type ι be given.
Let x23 of type ι be given.
Let x24 of type ι be given.
Let x25 of type ι be given.
Let x26 of type ι be given.
Let x27 of type ι be given.
Let x28 of type ι be given.
Let x29 of type ι be given.
Let x30 of type ι be given.
Let x31 of type ι be given.
Let x32 of type ι be given.
Let x33 of type ι be given.
Let x34 of type ι be given.
Let x35 of type ι be given.
Let x36 of type ι be given.
Let x37 of type ι be given.
Let x38 of type ι be given.
Let x39 of type ι be given.
Let x40 of type ι be given.
Let x41 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: SNo x3.
Assume H4: SNo x4.
Assume H5: SNo x5.
Assume H6: SNo x6.
Assume H7: SNo x7.
Assume H8: SNo x8.
Assume H9: SNo x9.
Assume H10: SNo x10.
Assume H11: SNo x11.
Assume H12: SNo x12.
Assume H13: SNo x13.
Assume H14: SNo x14.
Assume H15: SNo x15.
Assume H16: SNo x16.
Assume H17: SNo x17.
Assume H18: SNo x18.
Assume H19: SNo x19.
Assume H20: SNo x20.
Assume H21: SNo x21.
Assume H22: SNo x22.
Assume H23: SNo x23.
Assume H24: SNo x24.
Assume H25: SNo x25.
Assume H26: SNo x26.
Assume H27: SNo x27.
Assume H28: SNo x28.
Assume H29: SNo x29.
Assume H30: SNo x30.
Assume H31: SNo x31.
Assume H32: SNo x32.
Assume H33: SNo x33.
Assume H34: SNo x34.
Assume H35: SNo x35.
Assume H36: SNo x36.
Assume H37: SNo x37.
Assume H38: SNo x38.
Assume H39: SNo x39.
Assume H40: SNo x40.
Assume H41: SNo x41.
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: ...
...
Claim L103: ...
...
Claim L104: ...
...
Claim L105: ...
...
Claim L106: ...
...
Claim L107: ...
...
Claim L108: ...
...
Claim L109: ...
...
Claim L110: ...
...
Claim L111: ...
...
Claim L112: ...
...
Claim L113: ...
...
Claim L114: ...
...
Claim L115: ...
...
Claim L116: ...
...
Claim L117: ...
...
Claim L118: ...
...
Claim L119: ...
...
Claim L120: ...
...
Claim L121: ...
...
Assume H122: SNoLt (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (add_SNo x39 (add_SNo x40 x41)))))))))))))))))))) 0.
Assume H123: SNoLe (add_SNo x1 (minus_SNo x0)) x21.
Assume H124: SNoLe (add_SNo x2 (minus_SNo x1)) x22.
Assume H125: SNoLe (add_SNo x3 (minus_SNo x2)) x23.
Assume H126: SNoLe (add_SNo x4 (minus_SNo x3)) x24.
Assume H127: SNoLe (add_SNo x5 (minus_SNo x4)) x25.
Assume H128: SNoLe (add_SNo x6 (minus_SNo x5)) x26.
Assume H129: SNoLe (add_SNo x7 (minus_SNo x6)) x27.
Assume H130: SNoLe (add_SNo x8 (minus_SNo x7)) x28.
Assume H131: SNoLe (add_SNo x9 (minus_SNo x8)) x29.
Assume H132: SNoLe (add_SNo x10 (minus_SNo x9)) x30.
Assume H133: SNoLe (add_SNo x11 (minus_SNo x10)) x31.
Assume H134: SNoLe (add_SNo x12 (minus_SNo x11)) x32.
Assume H135: SNoLe (add_SNo ... ...) ....
...
■