-- ABPPROOFD


Derivation of

    fhead2(cs) = ok
==> trans(b,m,b,n,is,cs) = trans(not(b),head(is),b,n,tail(is),next1(ftail(cs)))

Applying the theorem

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

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

    All cs:
    (    fhead1(cs) = ok
       & fhead2(cs0) = ok
     |   fhead1(cs) = error
       & fhead2(cs0) = ok)
==> trans(b,m,b,n,is,cs0) = trans(not(b),head(is),b,n,tail(is),next1(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

      fhead1(ftail(cs0)) = ok
    & fhead2(cs0) = ok
==> trans(b,m,b,n,is,cs0) = trans(not(b),head(is),b,n,tail(is),next1(ftail(cs0)))

Applying the theorem

     next1(cs) = cs
<=== fhead1(cs) = ok

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

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

Applying the theorem

     trans(b,m,b,n,is,cs) = trans(not(b),head(is),b,n,tail(is),ftail(cs))
<=== fhead2(cs) = ok

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

      fhead1(ftail(cs0)) = error
    & fhead2(cs0) = ok
==> trans(b,m,b,n,is,cs0) = trans(not(b),head(is),b,n,tail(is),next1(ftail(cs0)))

Applying the theorem

     trans(b,m,b,n,is,cs) = trans(not(b),head(is),b,n,tail(is),ftail(cs))
<=== fhead2(cs) = ok

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

      fhead1(ftail(cs0)) = error
    & fhead2(cs0) = ok
==> trans(not(b2),head(is2),b2,n2,tail(is2),ftail(cs0)) = trans(not(b2),head(is2),b2,n2,tail(is2),next1(ftail(cs0)))

Applying the theorem

     next1(cs) = next1(ftail(cs))
<=== fhead1(cs) = error

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

      fhead1(ftail(cs0)) = error
    & fhead2(cs0) = ok
==> trans(not(b2),head(is2),b2,n2,tail(is2),ftail(cs0)) = trans(not(b2),head(is2),b2,n2,tail(is2),next1(ftail(ftail(cs0))))

Applying the theorem

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

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

      fhead1(ftail(cs0)) = error
    & fhead2(cs0) = ok
==> not(b2) =/= b2

Applying the theorem

not(b) =/= b

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

True

Number of proof steps: 8