Ancestors of theory Proof

The name of every theory is linked to its theory file
\/ stands for subtheories (child theories)
/\ stands for supertheories (parent theories)
... stands for repeated subtrees

Back to the index of BV_ASCII 

Proof \/
 \__Correct \//\
     \__WT \//\
         \__Convert \//\
             \__Types \//\
                 \__WellForm \//\
                 |   \__Classfile \//\
                 |   |   \__Cpool \//\
                 |   |   |   \__Data \//\
                 |   |   |       \__Basic \//\
                 |   |   |           \__Main \//\
                 |   |   |               \__Map \//\
                 |   |   |               |   \__List \//\
                 |   |   |               |   |   \__Datatype \//\
                 |   |   |               |   |   |   \__Univ \//\
                 |   |   |               |   |   |       \__Arith \//\
                 |   |   |               |   |   |       |   \__Nat \//\
                 |   |   |               |   |   |       |       \__NatDef \//\
                 |   |   |               |   |   |       |       |   \__WF \//\
                 |   |   |               |   |   |       |       |       \__Trancl \//\
                 |   |   |               |   |   |       |       |           \__Lfp \//\
                 |   |   |               |   |   |       |       |           |   \__mono \//\
                 |   |   |               |   |   |       |       |           |   |   \__equalities \//\
                 |   |   |               |   |   |       |       |           |   |       \__subset \//\
                 |   |   |               |   |   |       |       |           |   |           \__Fun \//\
                 |   |   |               |   |   |       |       |           |   |               \__Vimage \//\
                 |   |   |               |   |   |       |       |           |   |                   \__Set \//\
                 |   |   |               |   |   |       |       |           |   |                       \__Ord \//\
                 |   |   |               |   |   |       |       |           |   |                           \__HOL \//\
                 |   |   |               |   |   |       |       |           |   |                               \__CPure \/
                 |   |   |               |   |   |       |       |           |   \__Prod \//\
                 |   |   |               |   |   |       |       |           |       \__Fun...\//\
                 |   |   |               |   |   |       |       |           \__Relation \//\
                 |   |   |               |   |   |       |       |               \__Prod...\//\
                 |   |   |               |   |   |       |       \__Inductive \//\
                 |   |   |               |   |   |       |           \__Gfp \//\
                 |   |   |               |   |   |       |           |   \__Lfp...\//\
                 |   |   |               |   |   |       |           \__Prod...\//\
                 |   |   |               |   |   |       \__Sum \//\
                 |   |   |               |   |   |           \__mono...\//\
                 |   |   |               |   |   \__WF_Rel \//\
                 |   |   |               |   |       \__Finite \//\
                 |   |   |               |   |           \__Divides \//\
                 |   |   |               |   |           |   \__Arith...\//\
                 |   |   |               |   |           \__Power \//\
                 |   |   |               |   |           |   \__Divides...\//\
                 |   |   |               |   |           \__Inductive...\//\
                 |   |   |               |   \__Option \//\
                 |   |   |               |       \__Datatype...\//\
                 |   |   |               \__Recdef \//\
                 |   |   |               |   \__WF_Rel...\//\
                 |   |   |               \__Record \//\
                 |   |   |               |   \__Datatype...\//\
                 |   |   |               \__Bin \//\
                 |   |   |               |   \__Int \//\
                 |   |   |               |   |   \__IntDef \//\
                 |   |   |               |   |       \__Equiv \//\
                 |   |   |               |   |       |   \__Relation...\//\
                 |   |   |               |   |       \__Arith...\//\
                 |   |   |               |   \__Datatype...\//\
                 |   |   |               \__RelPow \//\
                 |   |   |               |   \__Nat...\//\
                 |   |   |               \__Sexp \//\
                 |   |   |               |   \__Univ...\//\
                 |   |   |               \__String \//\
                 |   |   |                   \__List...\//\
                 |   |   \__Store \//\
                 |   |   |   \__Map...\//\
                 |   |   \__WF_Rel...\//\
                 |   \__Runtime \//\
                 |       \__Classfile...\//\
                 \__Exec \//\
                     \__LoadAndStore \//\
                     |   \__Runtime...\//\
                     \__Object \//\
                     |   \__Runtime...\//\
                     \__Method \//\
                     |   \__Runtime...\//\
                     \__Opstack \//\
                     |   \__Runtime...\//\
                     \__Control \//\
                     |   \__Runtime...\//\
                     \__RelPow...\//\