checkAnswer'Def :: Def
checkAnswer'Def =
    Def "checkAnswer'" ["Env0", "answer", "capacities", "reqLvl", "q1"] (
      ((V "answer" === C "nil" []) &&&
      (call "isFinishEnv" [V "Env0", V "reqLvl", V "q1"])) |||
      (fresh ["x", "xs"] (
         (V "answer" === C "%" [V "x", V "xs"]) &&&
         (fresh ["q3"] (
            (call "checkStep" [V "Env0", V "x", V "capacities", V "q3"]) &&&
            (((V "q3" === C "true" []) &&&
            (fresh ["q4"] (
               (call "doStep" [V "Env0", V "x", V "capacities", V "q4"]) &&&
               (call "checkAnswer'" [V "q4", V "xs", V "capacities", V "reqLvl", V "q1"])))) |||
            ((V "q3" === C "false" []) &&&
            (V "q1" === C "false" [])))))))
    )
checkAnswer'Def :: Def
checkAnswer'Def =
    Def "checkAnswer'" ["Env0", "answer", "capacities", "reqLvl", "q1"] (
      ((V "answer" === C "nil" []) &&&
      (call "isFinishEnv" [V "Env0", V "reqLvl", V "q1"])) |||
      (fresh ["x", "xs"] (
         (V "answer" === C "%" [V "x", V "xs"]) &&&
         (fresh ["q3"] (
            (call "checkStep" [V "Env0", V "x", V "capacities", V "q3"]) &&&
            (((V "q3" === C "true" []) &&&
            (fresh ["q4"] (
               (call "doStep" [V "Env0", V "x", V "capacities", V "q4"]) &&&
               (call "checkAnswer'" [V "q4", V "xs", V "capacities", V "reqLvl", V "q1"])))) |||
            ((V "q3" === C "false" []) &&&
            (V "q1" === C "false" [])))))))
    )
checkAnswer'Def =
    Def "checkAnswer'" ["Env0", "answer", "capacities", "reqLvl", "q1"] (
      ((V "answer" === C "nil" []) &&&
      (call "isFinishEnv" [V "Env0", V "reqLvl", V "q1"])) |||
      (fresh ["x", "xs"] (
         (V "answer" === C "%" [V "x", V "xs"]) &&&
         (fresh ["q3"] (
            (call "checkStep" [V "Env0", V "x", V "capacities", V "q3"]) &&&
            (((V "q3" === C "true" []) &&&
            (fresh ["q4"] (
               (call "doStep" [V "Env0", V "x", V "capacities", V "q4"]) &&&
               (call "checkAnswer'" [V "q4", V "xs", V "capacities", V "reqLvl", V "q1"])))) |||
            ((V "q3" === C "false" []) &&&
            (V "q1" === C "false" [])))))))
    )