-- PHIL2PROOF


Derivation of

All s:
(      safe(s)
     & s -> s'
 ==> safe(s'))

Narrowing the preceding formula leads to 

  (    ({a,b,c,d},{f1,f2,f3,f4},{}) -> s'
   ==> safe(s'))
& (    ({b,c,d},{f3,f4},{a}) -> s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({b,c,d},{f3,f4},{a})
   ==> safe({b,c,d},{f3,f4},{a}))
& (    s' = ({a,c,d},{f1,f4},{b})
   ==> safe({a,c,d},{f1,f4},{b}))
& (    s' = ({a,b,d},{f1,f2},{c})
   ==> safe({a,b,d},{f1,f2},{c}))
& (    s' = ({a,b,c},{f2,f3},{d})
   ==> safe({a,b,c},{f2,f3},{d}))
& (    ({b,c,d},{f3,f4},{a}) -> s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,c,d},{f1,f4},{b})
   ==> safe({a,c,d},{f1,f4},{b}))
& (    s' = ({a,b,d},{f1,f2},{c})
   ==> safe({a,b,d},{f1,f2},{c}))
& (    s' = ({a,b,c},{f2,f3},{d})
   ==> safe({a,b,c},{f2,f3},{d}))
& (    ({b,c,d},{f3,f4},{a}) -> s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,b,d},{f1,f2},{c})
   ==> safe({a,b,d},{f1,f2},{c}))
& (    s' = ({a,b,c},{f2,f3},{d})
   ==> safe({a,b,c},{f2,f3},{d}))
& (    ({b,c,d},{f3,f4},{a}) -> s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,b,c},{f2,f3},{d})
   ==> safe({a,b,c},{f2,f3},{d}))
& (    ({b,c,d},{f3,f4},{a}) -> s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({b,c,d},{f3,f4},{a}) -> s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({b,d},{},{a,c})
   ==> safe({b,d},{},{a,c}))
& (    ({b,c,d,a},{f3,f4}++forks(a),{}) = s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({b,c,d,a},{f3,f4}++forks(a),{}) = s'
   ==> safe(s'))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({b,c,d,a},{f3,f4,f1,f2},{})
   ==> safe({b,c,d,a},{f3,f4,f1,f2},{}))
& (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,c,d},{f1,f4},{b}) -> s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,c},{},{b,d})
   ==> safe({a,c},{},{b,d}))
& (    ({a,c,d,b},{f1,f4}++forks(b),{}) = s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,c,d,b},{f1,f4}++forks(b),{}) = s'
   ==> safe(s'))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,c,d,b},{f1,f4,f2,f3},{})
   ==> safe({a,c,d,b},{f1,f4,f2,f3},{}))
& (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,b,d},{f1,f2},{c}) -> s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({b,d},{},{c,a})
   ==> safe({b,d},{},{c,a}))
& (    ({a,b,d,c},{f1,f2}++forks(c),{}) = s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,b,d,c},{f1,f2}++forks(c),{}) = s'
   ==> safe(s'))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,b,d,c},{f1,f2,f3,f4},{})
   ==> safe({a,b,d,c},{f1,f2,f3,f4},{}))
& (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,b,c},{f2,f3},{d}) -> s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,c},{},{d,b})
   ==> safe({a,c},{},{d,b}))
& (    ({a,b,c,d},{f2,f3}++forks(d),{}) = s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,b,c,d},{f2,f3}++forks(d),{}) = s'
   ==> safe(s'))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,b,c,d},{f2,f3,f4,f1},{})
   ==> safe({a,b,c,d},{f2,f3,f4,f1},{}))
& (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,c},{},{b,d}) -> s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,c,b},forks(b),{d}) = s'
   ==> safe(s'))
& (    ({a,c,d},forks(d),{b}) = s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,c,b},{f2,f3},{d})
   ==> safe({a,c,b},{f2,f3},{d}))
& (    ({a,c,d},forks(d),{b}) = s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({a,c,d},forks(d),{b}) = s'
   ==> safe(s'))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({a,c,d},{f4,f1},{b})
   ==> safe({a,c,d},{f4,f1},{b}))
& (    ({b,d},{},{a,c}) -> s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

    ({b,d},{},{a,c}) -> s'
==> safe(s')

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    ({b,d,a},forks(a),{c}) = s'
   ==> safe(s'))
& (    ({b,d,c},forks(c),{a}) = s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

  (    s' = ({b,d,a},{f1,f2},{c})
   ==> safe({b,d,a},{f1,f2},{c}))
& (    ({b,d,c},forks(c),{a}) = s'
   ==> safe(s'))

Reducts have been simplified.

Narrowing the preceding formula leads to 

    ({b,d,c},forks(c),{a}) = s'
==> safe(s')

Reducts have been simplified.

Narrowing the preceding formula leads to 

    s' = ({b,d,c},{f3,f4},{a})
==> safe({b,d,c},{f3,f4},{a})

Reducts have been simplified.

Narrowing the preceding formula leads to 

True

Reducts have been simplified.

Number of proof steps: 32

Solutions:

True