Unassignable-ABCDXYZ equivalency proof

Converting ABCDXYZ to :≠ is trivial. Below is a way to convert :≠ to ABCDXYZ.
For each object in a :≠ program, there are three things to do:
* Replace its declaration with one that declares just ABCD object(s).
* Replace its definition with definitions for each new ABCD object.
* Replace method calls on it with ones on the new ABCD object(s).
Once this is done, it is trivial to convert to ABCDXYZ... nearly.
:≠ allows initial values; ABCDXYZ sets everything to A. So we add an object named (say) unao_init, which sets every other object's initial value, then does main->call;; this becomes object number 0 in ABCDXYZ.
And io->output(c) is converted into "c.
== Types ==
Each type will be dealt with separately: 
* ABCD
* function
* integer
* unat_io -- made up name for io's type
* unat_bit -- new type to help convert integers (see below)
(Names starting with una are reserved for use of the implementation. Here, the prefix unat_ is used for new types and prefix unao_ for new objects.)
== ABCD ==
Nothing to do.
== unat_io ==
Cannot declare anything of this type.
== function ==
Let f be a function object. Then:
Declarations
 function f = activated; ==> ABCD unao_fun_f = B;
 function f = deactivated; ==> ABCD unao_fun_f = C;
Definition
 f { run { statements } } ==> unao_fun_f { event { statements } }
Method calls
 f -> activate; ==> unao_fun_f -> Z;
 f -> deactivate; ==> unao_fun_f -> Y;
 f -> call; ==> unao_fun_f -> X, Z;
(Note: obj -> m1, m2; is shorthand for obj -> m1; obj -> m2;.)
== unat_bit ==
A unat_bit is a one-bit integer, with the following methods:
 bit->toggle; Toggle bit. 
 bit->increment; Toggle bit. If it becomes clear, run the carry event.
 bit->decrement; Toggle bit. If it becomes set, run the borrow event.
 bit->loop; Run the iterate event.
 bit->loopifset; If currently set, run the iterateifset event.
A unat_bit is implemented with 4 ABCD objects, named (poorly and unimaginatively) a, b, c, and d:
a handles the carry event.
b handles the borrow event.
c handles the iterate event.
d handles the iterateifset event.
a, b and d's values are updated in tandem when the bit is toggled (c stays in state B).
Declarations
 unat_bit bit = init;
becomes (A_or_C = A if init==set, C if init==clear):
 ABCD unao_bita_bit = A_or_C;
 ABCD unao_bitb_bit = A_or_C;
 ABCD unao_bitc_bit = B;
 ABCD unao_bitd_bit = A_or_C;
Definitions
 bit {
 carry { stmts_carry }
 borrow { stmts_borrow }
 iterate { stmts_iterate }
 iterateifset { stmts_iterateifset }
 }
becomes
 unao_bita_bit { event { stmts_carry } }
 unao_bitb_bit { event { stmts_borrow } }
 unao_bitc_bit { event { stmts_iterate } }
 unao_bitd_bit { event { stmts_iterateifset } }
Method calls
 bit->toggle ==> unao_bita_bit->X, Y; unao_bitb_bit->X, Y; unao_bitd_bit->X, Y;
 bit->increment ==> unao_bita_bit->X, X; unao_bitb_bit->X, Y; unao_bitd_bit->X, Y;
 bit->decrement ==> unao_bita_bit->X, Y; unao_bitb_bit->Y, Y; unao_bitd_bit->X, Y;
 bit->loop ==> unao_bitc_bit->X, Z;
 bit->loopifset ==> unao_bitd_bit->X, X, X, Y;
== integer ==
Let x be an integer object. First, it is converted into individual unat_bits, which can be converted into ABCDs as above.
Declaration
 integer x(max) = init;
is converted to
 unat_bit unao_i0_x = init0
 unat_bit unao_i1_x = init1
 unat_bit unao_i2_x = init2
 unat_bit unao_i3_x = init3
 ...
 unat_bit unao_i(n-1)_x = init(n-1)
 
(where n is number of bits in max, and initk is kth bit of init.)
Definition
 x {
 overflow { stmts_overflow }
 underflow { stmts_underflow }
 iterate { stmts_iterate }
 }
is converted to
 unao_i0_x {
 carry { unao_i1_x->increment; }
 borrow { unao_i1_x->decrement; }
 iterate { stmts_iterate }
 iterateifset { stmts_iterate }
 }
 unao_i1_x {
 carry { unao_i2_x->increment; }
 borrow { unao_i2_x->decrement; }
 iterate { unao_i0_x->loop, loop; }
 iterateifset { unao_i0_x->loop, loop; }
 }
 
 ...
 
 unao_ik_x {
 carry { unao_i(k+1)_x->increment; }
 borrow { unao_i(k+1)_x->decrement; }
 iterate { unao_i(k-1)_x->loop, loop; }
 iterateifset { unao_i(k-1)_x->loop, loop; }
 }
 
 ...
 
 unao_i(n-2)_x {
 carry { unao_i(n-1)_x->increment; } 
 borrow { unao_i(n-1)_x->decrement; } 
 iterate { unao_i(n-3)_x->loop, loop; } 
 iterateifset { unao_i(n-3)_x->loop, loop; } 
 }
 unao_i(n-1)_x {
 carry { stmts_overflow }
 borrow { stmts_underflow }
 iterate { unao_i(n-2)_x->loop, loop; }
 iterateifset { unao_i(n-2)_x->loop, loop; }
 }
Method calls
 x -> increment(r);
 x -> decrement(r);
become (where r = 2 ** k)
 unao_ik_x -> increment;
 unao_ik_x -> decrement;
and
 x -> loop;
becomes
 unao_i0_x -> loopifset;
 unao_i1_x -> loopifset;
 unao_i2_x -> loopifset;
 ...
 unao_i(n-1)_x -> loopifset;
How does all this work?
When incrementing/decrementing x, it increments/decrements the bit required, and if there is a carry/borrow, the next highest bit is incremented/decremented. looping on x will loopifset on each of its bits. Each set bit k of x then performs x.iterate 2 ** k times, by looping the next-lower-order bit twice.
Example
Say x = 6 (dec) = 0110 (bin). So 
 x -> loop;
becomes
 unao_i0_x -> loopifset;
 unao_i1_x -> loopifset;
 unao_i2_x -> loopifset;
 unao_i3_x -> loopifset;
The 0th loopifset does nothing.
The 1st loopifset runs x.iterate 2 times.
The 2nd loopifset runs x.iterate 4 times.
The 3rd loopifset does nothing.
In all, x.iterate is run 6 times.
Category:Proofs