cryptol code to solve https://puzzling.stackexchange.com/q/83601/8871; use `cryptol 83601.cry -c ':sat isSolution'` to run it

83601.cry

isSolution w o n e = all isDigit [w,o,n,e] /\ no*won*won == wonewon /\ no != 0 where
	no = fromDigits [o,n]
	won = fromDigits [n,o,w]
	wonewon = fromDigits [n,o,w,e,n,o,w] : [32]

isDigit x = 0 <= x /\ x <= 9
fromDigits digits = sum [digit * 10^^exp | digit <- digits | exp <- [0...]]

And here's the output:

% cryptol 83601.cry -c ':sat isSolution'
Loading module Cryptol
Loading module Main
isSolution 0x00000001 0x00000003 0x00000007 0x00000000 = True
(Total Elapsed Time: 0.294s, using Z3)

👍