equal
deleted
inserted
replaced
48 Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts" |
48 Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts" |
49 Abs_Forest_inverse |
49 Abs_Forest_inverse |
50 "z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z" |
50 "z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z" |
51 |
51 |
52 (*the concrete constants*) |
52 (*the concrete constants*) |
53 TCONS_def "TCONS(M,N) == In0(M . N)" |
53 TCONS_def "TCONS(M,N) == In0(M $ N)" |
54 FNIL_def "FNIL == In1(NIL)" |
54 FNIL_def "FNIL == In1(NIL)" |
55 FCONS_def "FCONS(M,N) == In1(CONS(M,N))" |
55 FCONS_def "FCONS(M,N) == In1(CONS(M,N))" |
56 (*the abstract constants*) |
56 (*the abstract constants*) |
57 Tcons_def "Tcons(a,ts) == Abs_Tree(TCONS(Leaf(a), Rep_Forest(ts)))" |
57 Tcons_def "Tcons(a,ts) == Abs_Tree(TCONS(Leaf(a), Rep_Forest(ts)))" |
58 Fnil_def "Fnil == Abs_Forest(FNIL)" |
58 Fnil_def "Fnil == Abs_Forest(FNIL)" |