---

finite-run-lt-witness(r) ==
  x.let x1,x2 = x 
     in <prior-run-events(r;x1)
        , z,_.
           let _,%3 = member-mapfilter-witness() [0, x1) 
                      (t.let x,_ = r t 
                          in if x then tt else ff fi ) 
                      (t.<t
                          , let x,_ = r t 
                            in case x
                               of inl(y) =>
                                let _,x,_ = y in 
                                x
                                | inr(_) =>
                                let _,x,_ = "???" in 
                                x
                          >) 
                      z 
           in %3 let e1,_ = z in <e1, <e1, , >, , >
        >

---

Definitions occuring in Statement :  prior-run-events: prior-run-events(r;t),  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  it: ,  spreadn: spread3,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  token: "$token",  from-upto: [n, m),  member-mapfilter-witness: member-mapfilter-witness()
Definitions :  prior-run-events: prior-run-events(r;t),  member-mapfilter-witness: member-mapfilter-witness(),  from-upto: [n, m),  natural_number: $n,  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spreadn: spread3,  token: "$token",  apply: f a,  spread: spread def,  pair: <a, b>,  it:
FDL editor aliases :  finite-run-lt-witness
Date html generated: 2011_08_17-PM-03_37_24
Last ObjectModification: 2010_11_30-AM-00_34_05

Home Index