Proof step 72 from proof sortedchars-no-dups (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 73:

  ⊦ char ≠ 'N', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 74:

  ⊦ char ≠ 'O', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 75:

  ⊦ char ≠ 'P', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 76:

  ⊦ char ≠ 'Q', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 77:

  ⊦ char ≠ 'R', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 78:

  ⊦ char ≠ 'S', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 79:

  ⊦ char ≠ 'T', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 80:

  ⊦ char ≠ 'U', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 81:

  ⊦ char ≠ 'V', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 82:

  ⊦ char ≠ 'W', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 83:

  ⊦ char ≠ 'X', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 84:

  ⊦ char ≠ 'Y', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

• Proof step 85:

  ⊦ char ≠ 'Z', char ≠ '[' ∧ char ≠ ']' ∧ char ≠ '^' ∧ char ≠ '_' ∧ char ≠ 'a' ∧ char ≠ 'b' ∧ char ≠ 'c' ∧ char ≠ 'd' ∧ char ≠ 'e' ∧ char ≠ 'f' ∧ char ≠ 'g' ∧ char ≠ 'h' ∧ char ≠ 'i' ∧ char ≠ 'j' ∧ char ≠ 'k' ∧ char ≠ 'l' ∧ char ≠ 'm' ∧ char ≠ 'n' ∧ char ≠ 'o' ∧ char ≠ 'p' ∧ char ≠ 'q' ∧ char ≠ 'r' ∧ char ≠ 's' ∧ char ≠ 't' ∧ char ≠ 'u' ∧ char ≠ 'v' ∧ char ≠ 'w' ∧ char ≠ 'x' ∧ char ≠ 'y' ∧ char ≠ 'z' ∧ char ≠ '|' ∧ char ≠ '~'

Rule argument

Additional information