1) Abridged problem statement
- An addition rebus replaces letters by digits 0–9 so that equal letters get equal digits, different letters get different digits, numbers don’t start with 0 (unless the number is zero), and the addition holds.
- A proper rebus has exactly one solution. An aligned rebus has all three numbers of the same length.
- Output 1000 different proper aligned addition rebuses (difference is up to letter relabeling; two rebuses are the same if a bijection on letters turns one into the other). Each line ≤ 100 characters. Input is empty.

2) Detailed editorial
Goal: Construct 1000 pairwise non-isomorphic aligned rebuses, each with a unique solution.

Key idea:
- Force a total order and exact values for nine letters A..I by using columns that:
  - forbid carries,
  - enforce “successor” constraints that make A..I map uniquely to 1..9.

Building one rebus:
- Fix a string perm as a permutation of the 8 letters A..H.
- Construct three 16-digit numbers L, R, S (aligned):
  For i = 0..7 (total 8 pairs of columns):
  - Column 2i (buffer/no-carry): L digit A, R digit A, S digit B. This encodes A + A = B with no carry.
  - Column 2i+1 (order constraint): L digit A, R digit perm[i], S digit next(perm[i]) in the alphabet. This encodes A + X = X+1 with no carry.

Why no carries ever occur:
- Let val(X) denote the digit assigned to X. We will prove val(A)=1 and val(X)=position(X) in A..I.
- Check per column without assuming val(A)=1:
  - A + A = B gives val(B) = 2·val(A) ≤ 9, hence val(A) ≤ 4.
  - For X ∈ {A..H}, A + X = X+1 implies val(X+1) = val(A)+val(X), so the sequence is arithmetic:
    val(B)=2·val(A), val(C)=3·val(A), …, val(I)=9·val(A).
  - Since digits are ≤ 9 and all must be distinct, the only possibility is val(A)=1 and thus val(B)=2, …, val(I)=9. Therefore, every column sums to at most 9 with zero carry, and there is no incoming or outgoing carry anywhere.

Why uniqueness (properness):
- The constraints force val(A)=1 and then uniquely val(B)=2, …, val(I)=9. No other digits are used. This is the only solution, so the rebus is proper.

Why pairwise non-isomorphic:
- Every output line follows the same 16-column pattern, but the 8 “order-constraining” columns (A + X = X+1) appear in the order dictated by perm. Two different permutations produce different strings.
- To map one rebus to another by a bijection on letters, the mapping must preserve every character position. The positions of the many ‘A’s and ‘B’s force f(A)=A and f(B)=B. From A + X = X+1 at identical positions, the mapping must further preserve the “+1” adjacency across A..I, which makes f the identity on A..I. Therefore, two different permutations cannot be mapped to each other; all printed rebuses are pairwise different under the problem’s equivalence.

Length bound:
- Each number has 16 digits; the line length is 16 + 1 + 16 + 1 + 16 = 50 ≤ 100.

Generating 1000:
- Start from perm="ABCDEFGH" and iterate 1000 times over next lexicographic permutations, emitting one rebus per permutation.

Complexity:
- O(1000) lines; per line O(1) work. Trivial for the limits.

3) Provided C++ solution with detailed comments

```cpp
#include <bits/stdc++.h>  // Pulls in most standard headers (convenient for contests)

using namespace std;

// Streaming operator for pair<T1, T2> (unused in this solution, but commonly added in templates)
template<typename T1, typename T2>
ostream& operator<<(ostream& out, const pair<T1, T2>& x) {
    return out << x.first << ' ' << x.second;
}

// Input operator for pair<T1, T2> (unused here)
template<typename T1, typename T2>
istream& operator>>(istream& in, pair<T1, T2>& x) {
    return in >> x.first >> x.second;
}

// Input operator for vector<T> (unused here)
template<typename T>
istream& operator>>(istream& in, vector<T>& a) {
    for(auto& x: a) {
        in >> x;
    }
    return in;
};

// Output operator for vector<T> (unused here)
template<typename T>
ostream& operator<<(ostream& out, const vector<T>& a) {
    for(auto x: a) {
        out << x << ' ';
    }
    return out;
};

// Emit 1000 different proper aligned rebuses
void solve() {
    // Idea:
    // - Force unique mapping by ensuring A=1, B=2, ..., I=9.
    // - Use 8 constraints A + X = X+1 (for X in A..H) interleaved with "buffer" columns A + A = B.
    // - The buffer columns guarantee no carry enters the next constraint column.
    // - Permuting the order of the 8 constraints yields pairwise non-isomorphic rebuses.

    string perm = "ABCDEFGH"; // the set of X letters used in A + X = X+1

    for(int steps = 0; steps < 1000; steps++) {
        // Move to the next permutation so each iteration prints a different pattern.
        // 8! = 40320 > 1000, so this is safe.
        next_permutation(perm.begin(), perm.end());

        string l, r, result;  // the three aligned numbers: l + r = result
        for(int i = 0; i < 8; i++) {
            // Column 2*i: buffer column "A + A = B"
            l.push_back('A');      // L's digit is 'A'
            l.push_back('A');      // Column 2*i+1 (below) will also start with 'A'

            r.push_back('A');      // R's digit is 'A' (buffer)
            r.push_back(perm[i]);  // Constraint column: R uses perm[i] at 2*i+1

            result.push_back('B');             // Buffer result: 'B' (so A+A=B)
            result.push_back(perm[i] + 1);     // Constraint result: next letter (X+1)
        }
        // Print one rebus: all three numbers are 16 chars long and aligned.
        cout << l << "+" << r << "=" << result << endl;
    }
}

int main() {
    ios_base::sync_with_stdio(false); // Fast I/O
    cin.tie(nullptr);                 // Untie cin from cout

    int T = 1;                        // Only one run (input is empty)
    // cin >> T;                      // Unused; the input is empty per statement
    for(int test = 1; test <= T; test++) {
        // cout << "Case #" << test << ": "; // Not needed
        solve();                           // Emit the 1000 rebuses
    }

    return 0; // Done
}
```

4) Python solution with detailed comments

```python
# We generate 1000 proper aligned addition rebuses using the same construction:
# - Each rebus consists of three 16-letter numbers L, R, S with
#   for i in 0..7:
#     column 2*i   : A + A = B        (buffer: ensures no carry)
#     column 2*i+1 : A + X = X+1      (order constraint; X ∈ A..H in a permuted order)
# This forces A=1, B=2, ..., I=9 uniquely (properness), and permuting the order
# of the 8 constraints yields pairwise non-isomorphic rebuses.

import sys

def next_permutation(seq):
    """
    In-place next lexicographic permutation on a list of comparable items.
    Returns True if the permutation was advanced, False if seq was the last permutation.
    """
    # 1) Find the largest i such that seq[i] < seq[i+1]
    i = len(seq) - 2
    while i >= 0 and seq[i] >= seq[i + 1]:
        i -= 1
    if i < 0:
        # Already the last permutation
        seq.reverse()
        return False

    # 2) Find the largest j > i such that seq[j] > seq[i]
    j = len(seq) - 1
    while seq[j] <= seq[i]:
        j -= 1

    # 3) Swap i and j
    seq[i], seq[j] = seq[j], seq[i]

    # 4) Reverse the suffix starting at i+1
    seq[i + 1:] = reversed(seq[i + 1:])
    return True

def solve():
    perm = list("ABCDEFGH")  # X ∈ {A..H}
    out = []
    for _ in range(1000):
        # Advance to the next permutation first (like the C++ code)
        next_permutation(perm)

        # Build the three aligned strings L, R, S (length 16)
        L_chars = []
        R_chars = []
        S_chars = []
        for i in range(8):
            # Buffer column: A + A = B
            L_chars.append('A')
            R_chars.append('A')
            S_chars.append('B')

            # Constraint column: A + X = X+1
            L_chars.append('A')
            R_chars.append(perm[i])
            S_chars.append(chr(ord(perm[i]) + 1))  # next letter

        L = "".join(L_chars)
        R = "".join(R_chars)
        S = "".join(S_chars)
        out.append(f"{L}+{R}={S}")

    sys.stdout.write("\n".join(out))

if __name__ == "__main__":
    solve()
```

5) Compressed editorial
- Use letters A..I mapped to digits 1..9. Construct 16-column aligned sums composed of 8 pairs:
  - Column 2i: A + A = B
  - Column 2i+1: A + X = X+1 for X in a permutation of A..H
- From these equalities, val(B)=2·val(A), val(C)=3·val(A), …, val(I)=9·val(A). Digit bounds and distinctness force val(A)=1, hence A..I map uniquely to 1..9 (properness). Every column’s sum ≤ 9, so there are no carries.
- Different permutations place the “A + X = X+1” columns in different positions; letter relabeling cannot reorder columns, and the fixed positions of many ‘A’s and ‘B’s force the identity mapping, making all outputs pairwise non-isomorphic.
- Each line has 16+1+16+1+16 = 50 characters ≤ 100. Printing 1000 such lines is trivial.