equal
deleted
inserted
replaced
14 B :: "i => i => i" |
14 B :: "i => i => i" |
15 C :: "i => i" |
15 C :: "i => i" |
16 |
16 |
17 definition |
17 definition |
18 Gamma :: "[i,i,i] => i" ("\<Gamma>") |
18 Gamma :: "[i,i,i] => i" ("\<Gamma>") |
19 "\<Gamma>(b,cden) = |
19 "\<Gamma>(b,cden) == |
20 (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union> |
20 (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union> |
21 {io \<in> id(loc->nat). B(b,fst(io))=0})" |
21 {io \<in> id(loc->nat). B(b,fst(io))=0})" |
22 |
22 |
23 primrec |
23 primrec |
24 "A(N(n), sigma) = n" |
24 "A(N(n), sigma) = n" |