module proof

import StdEnv, StdDebug

from Data.Func import $
import Data.Maybe

import Smurf, SmurfParse

Start = toString (devtree ass) +++ "\n"
where
	ass (pgm, ip, st)
		| pgm == [Tail,Tail] && st.stack == [Lit "bcd"]
			= Just ([], [], {st & stack=[Lit "d"]})
		= Nothing
	pgm = fromJust $ parse ['ittt']
	devtree ass
		= fromJust (prover ass pgm zero { zero & input = [Lit "abcd"] } listIO)