diff --git a/src/Main.elm b/src/Main.elm
index f9342dd..c17209a 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -33,19 +33,31 @@ type EditMode
     = Query
     | Syntax
 
-modeEq : EditMode -> EditMode -> Bool
-modeEq m1 m2 =
+editModeEq : EditMode -> EditMode -> Bool
+editModeEq m1 m2 =
     case (m1, m2) of
         (Query, Query) -> True
         (Syntax, Syntax) -> True
         _ -> False
 
+type ResultMode
+    = Conclusion
+    | Tree
+
+resultModeEq : ResultMode -> ResultMode -> Bool
+resultModeEq rm1 rm2 =
+    case (rm1, rm2) of
+        (Conclusion, Conclusion) -> True
+        (Tree, Tree) -> True
+        _ -> False
+
 type alias Model =
     { program : String
     , renderProgram: String
-    , query : String
     , tab : Tab
+    , query : String
     , editMode : EditMode
+    , resultMode : ResultMode
     }
 type alias Flags = { renderRules: String, rules: String, query: String }
 type Msg
@@ -54,9 +66,10 @@ type Msg
     | SetQuery String
     | SetTab Tab
     | SetEditMode EditMode
+    | SetResultMode ResultMode
 
 init : Flags -> (Model, Cmd Msg)
-init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
+init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
 
 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@@ -82,7 +95,10 @@ viewTabSelector : Tab -> List (Tab, String) -> Html Msg
 viewTabSelector = viewSelector tabEq SetTab
 
 viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
-viewEditModeSelector = viewSelector modeEq SetEditMode
+viewEditModeSelector = viewSelector editModeEq SetEditMode
+
+viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
+viewResultModeSelector = viewSelector resultModeEq SetResultMode
 
 viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
 viewRule env r = renderRuleViaRules env r
@@ -99,48 +115,58 @@ viewRuleSection env sec =
         ])
 
 viewRules : String -> String -> Html Msg
-viewRules renderProgs progs = viewSection "Rendered Rules" <|
+viewRules renderProgs progs =
     Html.div [ class "bergamot-section-list" ] <|
         case (run program renderProgs, run program progs) of
             (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
             _ -> []
 
 proofGoal : EditMode -> String -> Maybe (Term Metavariable)
-proofGoal mode querys =
-    case mode of
+proofGoal editMode querys =
+    case editMode of
         Query -> run term querys
         Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
 
 tryProve : EditMode -> String -> String -> Maybe ProofTree
-tryProve mode progs querys =
-    case (run program progs, proofGoal mode querys) of
+tryProve editMode progs querys =
+    case (run program progs, proofGoal editMode querys) of
         (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
         _ -> Nothing
 
-viewProofTree : EditMode -> String -> String -> String -> Html Msg
-viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
+viewProofTree : EditMode -> ResultMode -> String -> String -> String -> Html Msg
+viewProofTree editMode resultMode renderProgs progs querys =
     Html.div [ class "bergamot-proof-tree" ] <|
-        case tryProve mode progs querys of
-            Just tree ->
+        case tryProve editMode progs querys of
+            Just (MkProofTree tree) ->
                 case run program renderProgs of
                     Just renderProg ->
-                        List.map latex
-                            <| List.filterMap (renderTreeViaRules renderProg)
-                            <| [ tree ]
+                        let
+                            maybeLatexString =
+                                case resultMode of
+                                    Conclusion -> renderTermViaRules renderProg (quoteVariables tree.conclusion)
+                                    Tree -> renderTreeViaRules renderProg (MkProofTree tree)
+                        in List.filterMap (Maybe.map latex) [maybeLatexString]
                     Nothing -> []
             Nothing -> []
 
 
 view : Model -> Html Msg
 view m = Html.div [ class "bergamot-root" ]
-    [ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta Rule Editor"), (Rendered, "Rendered Rules")]
-    , viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
-    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
-    , viewProofTree m.editMode m.renderProgram m.program m.query
-    , viewTab m.tab
-        (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
-        (viewSection "Meta Rules" <| Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
-        (Html.Lazy.lazy2 viewRules m.renderProgram m.program)
+    [ viewSection "Input" <| Html.div []
+        [ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
+        , Html.input [ type_ "text", onInput SetQuery, value m.query ] []
+        ]
+    , viewSection "Result" <| Html.div[]
+        [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
+        , viewProofTree m.editMode m.resultMode m.renderProgram m.program m.query
+        ]
+    , viewSection "Rules" <| Html.div []
+        [ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]
+        , viewTab m.tab
+            (Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
+            (Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
+            (Html.Lazy.lazy2 viewRules m.renderProgram m.program)
+        ]
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)
@@ -151,6 +177,7 @@ update msg m =
         SetQuery query -> ({ m | query = query }, Cmd.none)
         SetTab tab -> ({ m | tab = tab }, Cmd.none)
         SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
+        SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
 
 subscriptions : Model -> Sub Msg
 subscriptions _ = Sub.none