-- ABPPROOFE


Derivation of

      b =/= b'
    & fhead1(cs) = ok
==> tail(trans(b,m,b',n,is,cs)) = trans(b,m,b,m,is,next2(ftail(cs)))

Applying the theorem

     True
===>   fhead2(cs) = ok
     | fhead2(cs) = error

at position [] of the preceding formula leads to the formula

    All cs:
    (    fhead2(cs) = ok
       & b =/= b'
       & fhead1(cs0) = ok
     |   fhead2(cs) = error
       & b =/= b'
       & fhead1(cs0) = ok)
==> tail(trans(b,m,b',n,is,cs0)) = trans(b,m,b,m,is,next2(ftail(cs0)))

Substituting ftail(cs0) for cs at position [0,0] of the preceding formula leads to 2 factors. The current factor is given by

      fhead2(ftail(cs0)) = ok
    & b =/= b'
    & fhead1(cs0) = ok
==> tail(trans(b,m,b',n,is,cs0)) = trans(b,m,b,m,is,next2(ftail(cs0)))

Applying the theorem

     next2(cs) = cs
<=== fhead2(cs) = ok

at position [1,1,5] of the preceding factor leads to the factor

      fhead2(ftail(cs0)) = ok
    & b =/= b'
    & fhead1(cs0) = ok
==> tail(trans(b,m,b',n,is,cs0)) = trans(b,m,b,m,is,ftail(cs0))

Applying the theorem

     tail(trans(b,m,b',n,is,cs)) = trans(b,m,b,m,is,ftail(cs))
<===   b =/= b'
     & fhead1(cs) = ok

at position [1] of the preceding factor leads to a single formula, which is given by

      fhead2(ftail(cs0)) = error
    & b =/= b'
    & fhead1(cs0) = ok
==> tail(trans(b,m,b',n,is,cs0)) = trans(b,m,b,m,is,next2(ftail(cs0)))

Applying the theorem

     tail(trans(b,m,b',n,is,cs)) = trans(b,m,b,m,is,ftail(cs))
<===   b =/= b'
     & fhead1(cs) = ok

at position [1,0] of the preceding formula leads to the formula

      fhead2(ftail(cs0)) = error
    & b1 =/= b'1
    & fhead1(cs0) = ok
==> trans(b1,m1,b1,m1,is1,ftail(cs0)) = trans(b1,m1,b1,m1,is1,next2(ftail(cs0)))

Applying the theorem

     next2(cs) = next2(ftail(cs))
<=== fhead2(cs) = error

at position [1,1,5] of the preceding formula leads to the formula

      fhead2(ftail(cs0)) = error
    & b1 =/= b'1
    & fhead1(cs0) = ok
==> trans(b1,m1,b1,m1,is1,ftail(cs0)) = trans(b1,m1,b1,m1,is1,next2(ftail(ftail(cs0))))

Applying the theorem

     trans(b,m,b,n,is,cs) = trans(b,m,b,n,is,next2(ftail(cs)))
<=== fhead2(cs) = error

at position [1] of the preceding formula leads to the formula

True

Number of proof steps: 7