-- PHIL1PROOF


Derivation of

loop[source]

Narrowing the preceding formula leads to 

loop[({a,b,c,d},{f1,f2,f3,f4},{})]

Reducts have been simplified.

Narrowing the preceding formula leads to 

  loop[({b,c,d},{f3,f4},{a}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,c,d},{f1,f4},{b}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,d},{f1,f2},{c}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,c},{f2,f3},{d}),({a,b,c,d},{f1,f2,f3,f4},{})]

Reducts have been simplified.

Narrowing the preceding formula leads to 

  loop[({b,d},{},{a,c}),({b,c,d},{f3,f4},{a}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,c,d},{f1,f4},{b}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,d},{f1,f2},{c}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,c},{f2,f3},{d}),({a,b,c,d},{f1,f2,f3,f4},{})]

Reducts have been simplified.

Narrowing the preceding formula leads to 

  loop[({b,d,a},{f1,f2},{c}),({b,d},{},{a,c}),({b,c,d},{f3,f4},{a}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,c,d},{f1,f4},{b}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,d},{f1,f2},{c}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,c},{f2,f3},{d}),({a,b,c,d},{f1,f2,f3,f4},{})]

Reducts have been simplified.

Narrowing the preceding formula leads to 

  loop[({b,d,a},{f1,f2},{c}),({b,d},{},{a,c}),({b,c,d},{f3,f4},{a}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,c},{},{b,d}),({a,c,d},{f1,f4},{b}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,d},{f1,f2},{c}),({a,b,c,d},{f1,f2,f3,f4},{})]
| loop[({a,b,c},{f2,f3},{d}),({a,b,c,d},{f1,f2,f3,f4},{})]

Reducts have been simplified.

Narrowing the preceding formula leads to 

True

Reducts have been simplified.

Number of proof steps: 6

Solutions:

True