[[[[[
   FUNDAMENTAL DECOMPOSITION
   We prove here that 
      H(y|x) <= H_C(x,y) - H(x) + c
]]]]]

define (all-together x*)

let c debug 100 [constant to satisfy Kraft (see lemma)]

let x debug run-utm-on debug x*

let H-of-x debug length x*

[programs we've discovered that calculate pairs 
 starting with x]
let programs nil

let (stage n)
    [generate requirements for all new programs we've
     discovered that produce (x y) pairs]
    let programs 
        (add-to-set debug (halts? nil debug n) programs) 
    (stage + n 1)

[at stage n = 0, 1, 2, 3, ...]
[look at all programs with <=n bits that halt within time n]
[returns list of all of them that produce pairs (x y)]
let (halts? p bits-left)
   let v try n C p [C is eval read-exp if C = U]
   if = success car v (look-at cadr v)
   if = 0 bits-left nil
   append (halts? append p cons 0 nil - bits-left 1)
          (halts? append p cons 1 nil - bits-left 1)

[returns (p) if C(p) = (x y), otherwise ()]
let (look-at v)
   if (and (is-pair v) 
            = x car v ) cons p nil
      nil

[logical "and"]
let (and p q)
   if p q false

[is x a pair?]
let (is-pair? x)
   if atom x         false
   if atom cdr x     false
   if atom cdr cdr x true
                     false

[is an element in a set?]
let (is-in-set? element set)
   if atom set          false
   if = element car set true
   (is-in-set? element cdr set)

[forms set union avoiding duplicates, 
 and makes requirement for each new find]
let (add-to-set new old)
   if  atom new  old 
   let first-new car new
   let rest-new  cdr new
   if (is-in-set? first-new old) (add-to-set rest-new old)
   (do (make-requirement first-new)
       cons first-new (add-to-set rest-new old)
   )
       
[first argument discarded, done for side-effect only!]
let (do x y) y

[given new p such that C(p) = (x y), 
 we produce the requirement for C_x
 that there be a program for y that is |p|-H(x)+c bits long]
let (make-requirement p)
   display cons cadr cadr try no-time-limit C p 
           cons - + c length p H-of-x
                nil

let C ' [here eval read-exp gives U]
[test case special-purpose computer C here in place of U:] 
[C(00100001) with x-1 and y-1 0's gives pair (x xy)]
[loop function gives number of bits up to next 1 bit]
   let (loop n)
      if = 1 read-bit n
      (loop + n 1)
   let x (loop 1)
   let y (loop 1)
   cons x cons * x y nil

[HERE GOES!]
(stage 0)

define x* 3
length bits x* 

[give all-together x*]
try 60 cons cons "'
            cons all-together 
            nil                      
       cons cons "' 
            cons bits x* 
            nil 
       nil 
    nil

define x* 4
length bits x* 

[give all-together x*]
try 60 cons cons "'
            cons all-together 
            nil                      
       cons cons "' 
            cons bits x* 
            nil 
       nil 
    nil