|- ∀l e. push l e = e::l

|- (∀v0. pop [] v0 = []) ∧
   ∀h t n. pop (h::t) n = if n = 0 then h::t else pop t (n − 1)

|- (take1 0 [] = []) ∧
   (take1 0 (x::xs) = if 0 = 0 then [] else x::take1 (0 − 1) xs) ∧
   (take1 (SUC v2) (x::xs) =
    if SUC v2 = 0 then [] else x::take1 (SUC v2 − 1) xs)

|- ∀n l. take n l = if LENGTH l ≥ n then SOME (take1 n l) else NONE

|- (isNonTmnlSym (NTS v0) ⇔ T) ∧ (isNonTmnlSym (TS v) ⇔ F)

|- (∀s. sym2Str (TS s) = s) ∧ ∀s. sym2Str (NTS s) = s

|- ∀l r. ruleRhs (rule l r) = r

|- ∀l r. ruleLhs (rule l r) = l

|- (∀nt ptl. ptree2Sym (Node nt ptl) = NTS nt) ∧
   ∀tm. ptree2Sym (Leaf tm) = TS tm

|- ∀p r.
     buildTree p r =
     (let s = take (LENGTH r) (MAP (ptree2Sym o SND) p)
      in
        if s = NONE then
          NONE
        else if r = THE s then
          take (LENGTH r) (MAP SND p)
        else
          NONE)

|- ∀p l r.
     addRule p (rule l r) =
     (let x = buildTree p (REVERSE r)
      in
        if x = NONE then NONE else SOME (Node l (REVERSE (THE x))))

|- ∀stl. stackSyms stl = REVERSE (MAP FST (MAP FST stl))

|- (findItemInRules (item l1 (r1,[])) [] ⇔ F) ∧
   (findItemInRules (item l1 (r1,[])) (rule l2 r2::rst) ⇔ T) ∧
   (findItemInRules (item v4 (v8,v12::v13)) v2 ⇔ F)

|- (itemEqRuleList [] [] ⇔ T) ∧ (itemEqRuleList [] (v9::v10) ⇔ T) ∧
   (itemEqRuleList (v3::v4) [] ⇔ F) ∧
   (itemEqRuleList (v5::v6) (v15::v16) ⇔
    if LENGTH (v5::v6) ≠ LENGTH (v15::v16) then
      F
    else if findItemInRules (HD (v5::v6)) (v15::v16) then
      itemEqRuleList (TL (v5::v6)) (v15::v16)
    else
      F)

|- ∀sg red itl sym.
     getState (sg,red) itl sym =
     (let newitl = sg itl sym and rl = red itl (sym2Str sym)
      in
        case (newitl,rl) of
          ([],[]) => NA
        | ([],y::ys) => if LENGTH rl = 1 then REDUCE (HD rl) else NA
        | (x::xs,[]) => GOTO newitl
        | (x::xs,y'::ys') =>
            if itemEqRuleList (x::xs) (y'::ys') then
              REDUCE (HD rl)
            else
              NA)

|- ∀stl. stackSyms stl = REVERSE (MAP FST (MAP FST stl))

|- ∀eof oldSym inp stl csl.
     exitCond (eof,oldSym) (inp,stl,csl) ⇔
     stl ≠ [] ∧ (stackSyms stl = [oldSym]) ∧ (inp = [TS eof])

|- ∀inis sl. init inis sl = (sl,[],[inis])

|- doReduce m (sym::rst,os,(s,itl):: $rem) ru =
   if isNonTmnlSym sym then
     NONE
   else
     (let l = ruleLhs ru and r = ruleRhs ru in
      let ptree = addRule os ru
      in
        case ptree of
          NONE => NONE
        | SOME p =>
            (let newStk = pop os (LENGTH r) in
             let newStateStk = pop ((s,itl):: $rem) (LENGTH r)
             in
               if newStateStk = [] then
                 NONE
               else
                 (let topitl = SND (HD newStateStk) in
                  let nx = FST m topitl (NTS l)
                  in
                    if nx = [] then
                      NONE
                    else
                      (let ns = (NTS l,nx)
                       in
                         SOME
                           (sym::rst,[(ns,p)] ++ newStk,
                            push newStateStk ns)))))

|- parse mac (inp,os,(s,itl):: $rem) =
   case mac of
     NONE => NONE
   | SOME m =>
       case inp of
         [] => NONE
       | [e] =>
           (let newState = getState m itl e
            in
              case newState of
                REDUCE ru => doReduce m ([e],os,(s,itl):: $rem) ru
              | GOTO st => NONE
              | NA => NONE)
       | e::v4::v5 =>
           (let newState = getState m itl e
            in
              case newState of
                REDUCE ru => doReduce m (e::v4::v5,os,(s,itl):: $rem) ru
              | GOTO st =>
                  if isNonTmnlSym e then
                    NONE
                  else
                    SOME
                      (v4::v5,((e,st),Leaf (sym2Str e))::os,
                       push ((s,itl):: $rem) (e,st))
              | NA => NONE)

|- ∀initState eof oldS m sl.
     parser (initState,eof,oldS) m sl =
     (let out =
            OWHILE
              (λopt.
                 case opt of
                   NONE => F
                 | SOME s => ¬exitCond (eof,NTS oldS) s)
              (λopt.
                 case opt of
                   NONE => NONE
                 | SOME s =>
                     (λ(sli,stli,csli). parse m (sli,stli,csli)) s)
              (SOME (init initState sl))
      in
        case out of
          NONE => NONE
        | SOME NONE => SOME NONE
        | SOME (SOME (slo,[],cs)) => SOME NONE
        | SOME (SOME (slo,[(st1,pt)],cs)) => SOME (SOME pt)
        | SOME (SOME (slo,(st1,pt)::v21::v22,cs)) => SOME NONE)