∀ (motive : PosNum → PosNum → Prop) (x x_1 : PosNum),
  (∀ (a : PosNum), motive a PosNum.one) →
    (∀ (b : PosNum), motive PosNum.one b) →
      (∀ (a b : PosNum), motive a.bit0 b.bit0) →
        (∀ (a b : PosNum), motive a.bit0 b.bit1) →
          (∀ (a b : PosNum), motive a.bit1 b.bit0) → (∀ (a b : PosNum), motive a.bit1 b.bit1) → motive x x_1