-- ABPPROOFC


Derivation of

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

Selecting induction variables at position [] of the preceding formula leads to the formula

All b b' m n is:
(      b =/= b'
     & fhead1(!cs) = error
 ==> trans(b,m,b',n,is,ftail(!cs)) = trans(b,m,b',n,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 b b' m n is:
(    All cs:
     (    fhead1(cs) = ok
        & b =/= b'
        & fhead1(!cs) = error
      |   fhead1(cs) = error
        & b =/= b'
        & fhead1(!cs) = error)
 ==> trans(b,m,b',n,is,ftail(!cs)) = trans(b,m,b',n,is,next1(ftail(!cs))))

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

All b b' m n is:
(      fhead1(ftail(!cs)) = ok
     & b =/= b'
     & fhead1(!cs) = error
 ==> trans(b,m,b',n,is,ftail(!cs)) = trans(b,m,b',n,is,next1(ftail(!cs))))

Applying the theorem

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

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

All b b' m n is:
(      fhead1(ftail(!cs)) = error
     & b =/= b'
     & fhead1(!cs) = error
 ==> trans(b,m,b',n,is,ftail(!cs)) = trans(b,m,b',n,is,next1(ftail(!cs))))

Applying the theorem

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

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

All b b' m n is:
(      fhead1(ftail(!cs)) = error
     & b =/= b'
     & fhead1(!cs) = error
 ==> trans(b,m,b',n,is,ftail(!cs)) = trans(b,m,b',n,is,next1(ftail(ftail(!cs)))))

Applying the theorem

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

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

All b1 b'1 m1 n1 is1:
(      fhead1(ftail(!cs)) = error
     & b1 =/= b'1
     & fhead1(!cs) = error
 ==> trans(b1,m1,b'1,n1,is1,ftail(ftail(!cs))) = trans(b1,m1,b'1,n1,is1,next1(ftail(ftail(!cs)))))

Applying the induction hypothesis

     trans(b0,m0,b'0,n0,is0,ftail(cs0)) = trans(b0,m0,b'0,n0,is0,next1(ftail(cs0)))
<===   (  b0 =/= b'0
        & fhead1(cs0) = error)
     & !cs >> cs0

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

All b1 b'1:
(      fhead1(ftail(!cs)) = error
     & b1 =/= b'1
     & fhead1(!cs) = error
 ==> !cs >> ftail(!cs))

Applying the theorem

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

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

True

Number of proof steps: 8