result for | v | ≤ n. When | v | = n + 1, it is obvious that | lo(v) | ≤ n and | hi(v) | ≤ n. According to (*), the number of models of φ(v) equals to the sum of number of models of (∧l ∈ L(v)) ∧ ¬var(v) ∧ φ(lo(v)) and (∧l ∈ L(v)) ∧
var(v) ∧ φ(hi(v)). By the induction hypothesis and Definition 3, and the number of models of (∧l ∈ L(v)) ∧ ¬var(v) 
∧ φ(lo(v)) (resp. (∧l ∈ L(v)) ∧ var(v) ∧ φ(hi(v))) equals to Count(lo(v), X) / 2 | L(v) | + 1 (resp. Count(hi(v), X) / 2 | L(v) 
| + 1). So the induction hypothesis holds. It means that CT is satisfied. In Proposition 9, we will show that ROBDD-∞ satisfies CD. Then by Lemma A.3, A.4 and A.7 in [5], we know that ROBDD-∞ satisfies ME, CE and IM. ■
 

| procedure Count(v, X)  1: if G4(v) ≠ empty then return G4(v) endif 2: if v is a terminal node then  3: if v = ⊥ then G4(v) ← 0  4: else G4(v) ← 2| X | − | L(v) | 5: endif 6: else G4(v) ← (Count(lo(v), X) + Count(hi(v), X)) / 2 | L(v) | + 1 7: endif 8: return G4(v) Figure 8. The algorithm Count   |
|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|

We know that two broad areas in formal verification of hardware are distinguished: checking whether a combinational circuit complies with a given specification; checking whether a circuit's behavior conforms to certain desired properties. The former is a case of equivalence checking, while the latter is mostly a case of clausal entailment. So ROBDD-∞ is potential to be widely used in verification field. 

Note that we just need some fragment information (i.e., the size) of the implied literals in Count and we pre-record them in implied literals table so that we can visit a node of ROBDD-∞ in constant time. The same situation occurs in computing the minimum cardinality [3], which is useful in model-based diagnose, we only need an extra data unit in implied literals table to pre-record the number of negative literals in implied literals set. By Proposition 4, every OBDD-L can be transformed into the corresponding ROBDD-∞ in polytime, and then we have that: 
Corollary 2. OBDD-L satisfies CO, VA, CE, IM, EQ, CT and ME. 

| L       | CD   | FO   | SFO   | ∧C   | ∧BC   | ∨C   | ∨BC   | ¬C   |
|---------|------|------|-------|------|-------|------|-------|------|
| ROBDD   | √    | -    | √     | -    | √     | -    | √     | √    |
| ROBDD-∞ | √    | -    | -     | -    | ?     | -    | -     | -    |
| FBDD    | √    | -    | o     | -    | o     | -    | o     | √    |
| d-DNNF  | √    | o    | o     | o    | o     | o    | o     | ?    |

Table 2. The polytime transformations of ROBDD-∞. √ means "satisfies", 
means "does not satisfy", means "does not satisfy unless P = NP", and ? 

means "unknown". 

•
o Table 2 summarizes transformation-related properties of ROBDD-∞. Again, Properties of d-DNNF, FBDD 
and ROBDD are also showed here for comparison. 

Proposition 9. The results in Table 2 hold. 

Proof. CD: An algorithm is presented in Figure 9. With the cache G5, this function Condition-sub will terminate in polytime. And we have showed that Add-to-inf can terminate in polytime in the previous section. So the algorithm Condition has a polynomial time complexity. Moreover, we prove that the result of Condition-sub(v, T) is an OBDD-L equivalent to φ(v) | T by induction on the size of | v |. The case | v | = 1 is immediate. Assume that the output of Condition-sub(v, T) is an OBDD-L equivalent to φ(v) | T and VARS(u) ⊆ *VARS*(v) for | v | ≤ n. When | v | = n + 1, it is obvious that | lo(v) | ≤ n and | hi(v) | ≤ n. By (*) and Definition 6, we have that φ( ) | ( ( )) | (( ( ) | ( ( )) | ) ( ( ) | ( ( )) | )). *v T l L v T var v T lo v T var v T hi v T* = ∧ ∈ ∧¬ ∧ ∨ ∧ φ φ Line 13 guarantees that at least one child of u is non-False if u is non-terminal. Then by the induction hypothesis and Definition 3, the DAG with the root u is an OBDD-L such that φ(u) ⇔ φ(v) | T and VARS(u) ⊆ *VARS*(v). Note that L(v) \ T and L(v) ∩ ¬T ≠ ∅ are needed to be computed just once for the same sets of implied literals set with the use of implied literals table. This means that the implied literals table is helpful for saving the computing time of the logical operations such as conditioning, clausal entailment and so on. 