diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..030c40e153da903bc2b2ac6a7a5d2c47d118c251
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml
@@ -0,0 +1,35 @@
+[package]
+name = "bmachine"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[[bin]]
+name = "bmachine"
+test = false
+bench = false
+
+[dependencies]
+btypes = { path = "../btypes_bitvec" }
+
+[dependencies.bitvec]
+version = "1"
+default-features = false
+features = []
+
+[profile.release]
+#opt-level = 3
+panic = "abort"
+#lto = 'fat'
+codegen-units = 1
+debug = true
+lto = true
+opt-level = "s"
+
+[profile.dev]
+opt-level = 0
+panic = "abort"
+
+[profile.test]
+panic = "abort"
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/rust-toolchain.toml b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/rust-toolchain.toml
new file mode 100644
index 0000000000000000000000000000000000000000..271800cb2f3791b3adc24328e71c9e2550b439db
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/rust-toolchain.toml
@@ -0,0 +1,2 @@
+[toolchain]
+channel = "nightly"
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..df7a8fa938149962c1259983f3f0bec3fb6e61a4
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml
@@ -0,0 +1,28 @@
+[package]
+name = "bmachine_mc"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+btypes = { path = "../btypes_bitvec" }
+threadpool = "1.8.1"
+dashmap = "~5.1.0"
+derivative = "2.2.0"
+
+[profile.release]
+#opt-level = 3
+panic = "abort"
+#lto = 'fat'
+codegen-units = 1
+debug = true
+lto = true
+opt-level = "s"
+
+[profile.dev]
+opt-level = 0
+panic = "abort"
+
+[profile.test]
+panic = "abort"
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/rust-toolchain.toml b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/rust-toolchain.toml
new file mode 100644
index 0000000000000000000000000000000000000000..271800cb2f3791b3adc24328e71c9e2550b439db
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/rust-toolchain.toml
@@ -0,0 +1,2 @@
+[toolchain]
+channel = "nightly"
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
index 7981552852333dec5b344fdb5972c83ed8c2da6f..e216cb905ad83b09cdb9befaf83320b1fa0beb6c 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
@@ -92,7 +92,7 @@ impl<L, const LS: usize, R, const RS: usize, const SIZE: usize, const REL_SIZE:
         let mut result_arr = [false; SIZE];
         for idx in 0..SIZE {
             let crel = Self::from_idx(idx);
-            result_arr[idx] = self.subset(&crel);
+            result_arr[idx] = crel.subset(&self);
         }
         return BSet::<Self, SIZE>::const_from_arr(result_arr);
     }
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/Cargo.toml b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..573c9210b2b967fc696c4c22d1f65b88dba14d21
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/Cargo.toml
@@ -0,0 +1,11 @@
+[package]
+name = "btypes"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies.bitvec]
+version = "1"
+default-features = false
+features = []
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/bboolean.rs b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/bboolean.rs
new file mode 100644
index 0000000000000000000000000000000000000000..74a1812f4706d46433a8cdd0b14718712c6f1b31
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/bboolean.rs
@@ -0,0 +1,45 @@
+#![ allow( dead_code ) ]
+
+
+use crate::bset::{BSet, SetItem};
+
+pub type BBoolean = bool;
+
+impl SetItem<2> for BBoolean {
+    fn from_idx(idx: usize) -> Self {
+        match idx {
+            0 => false,
+            1 => true,
+            _ => panic!("Bool index {:?} out of range!", idx)
+        }
+    }
+    fn as_idx(&self) -> usize {
+        if *self { 1 } else { 0 }
+    }
+}
+
+pub const BOOL: BSet<bool, 2> = BSet::full();//BSet::const_from_arr([true, true]);
+
+pub trait BBool {
+    fn new(val: bool) -> BBoolean;
+    fn equal(&self, other: &Self) -> bool;
+    fn or(&self, other: &Self) -> Self;
+    fn xor(&self, other: &Self) -> Self;
+    fn and(&self, other: &Self) -> Self;
+    fn not(&self) -> Self;
+    fn implies<F: FnOnce() -> bool>(&self, other: F) -> Self;
+    fn equivalent(&self, other: &Self) -> Self;
+    fn unequal(&self, other: &Self) -> Self;
+}
+
+impl BBool for bool {
+    fn new(val: bool) -> BBoolean { val }
+    fn equal(&self, other: &Self) -> bool { *self == *other }
+    fn or(&self, other: &Self) -> Self { *self || *other }
+    fn xor(&self, other: &Self) -> Self { *self ^ *other }
+    fn and(&self, other: &Self) -> Self { *self && *other }
+    fn not(&self) -> Self { !*self }
+    fn implies<F: FnOnce() -> bool>(&self, other: F) -> Self { !*self || other() }
+    fn equivalent(&self, other: &Self) -> Self { *self == *other }
+    fn unequal(&self, other: &Self) -> Self { *self != *other }
+}
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/binteger.rs b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/binteger.rs
new file mode 100644
index 0000000000000000000000000000000000000000..0311a2545dba57cfc345e981713eb4edc986553b
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/binteger.rs
@@ -0,0 +1,98 @@
+#![allow(non_snake_case, non_camel_case_types)]
+
+use core::convert::TryInto;
+use crate::bboolean::BBoolean;
+use crate::bset::{BSet, SetItem};
+
+pub type BInteger = i128;
+pub type set_BInteger = BSet<BInteger, INTEGER_SIZE>;
+
+pub const LOWER_BOUND: BInteger = -10;
+pub const UPPER_BOUND: BInteger = 20;
+pub const INTEGER_SIZE: usize = 31; //UB - LB + 1
+
+pub trait BInt {
+    fn equal(&self, other: &Self) -> bool;
+    fn unequal(&self, other: &Self) -> bool;
+
+    fn greater(&self, other: &Self) -> bool;
+    fn greaterEqual(&self, other: &Self) -> bool;
+    fn less(&self, other: &Self) -> bool;
+    fn lessEqual(&self, other: &Self) -> bool;
+
+    fn plus(&self, other: &Self) -> Self;
+    fn minus(&self, other: &Self) -> Self;
+    fn multiply(&self, other: &Self) -> Self;
+    fn divide(&self, other: &Self) -> Self;
+    fn modulo(&self, other: &Self) -> Self;
+    fn power(&self, exp: &Self) -> Self;
+
+    fn negative(&self) -> Self;
+    fn pred(&self) -> Self;
+    fn succ(&self) -> Self;
+
+    fn from(source: BInteger) -> Self;
+    fn new(source: BInteger) -> Self;
+
+    fn isInteger(&self) -> BBoolean { true }
+    fn isNotInteger(&self) -> BBoolean { false }
+    fn isNatural(&self) -> BBoolean;
+    fn isNotNatural(&self) -> BBoolean;
+    fn isNatural1(&self) -> BBoolean;
+    fn isNotNatural1(&self) -> BBoolean;
+}
+
+impl BInt for BInteger {
+    fn equal(&self, other: &Self) -> bool { self.eq(&other) }
+    fn unequal(&self, other: &Self) -> bool { !self.eq(&other) }
+
+    fn greater(&self, other: &Self) -> bool { self > other }
+    fn greaterEqual(&self, other: &Self) -> bool { self >= other }
+    fn less(&self, other: &Self) -> bool { self < other }
+    fn lessEqual(&self, other: &Self) -> bool { self <= other }
+
+    fn plus(&self, other: &Self) -> Self { self + other }
+    fn minus(&self, other: &Self) -> Self { self - other }
+    fn multiply(&self, other: &Self) -> Self { self * other }
+    fn divide(&self, other: &Self) -> Self { self / other }
+    fn modulo(&self, other: &Self) -> Self { self % other }
+    fn power(&self, exp: &Self) -> Self {
+        if exp < &0 { panic!("Power with negative exponent!") }
+        let u32_exp: u32 = exp.unsigned_abs().try_into().unwrap();
+        return self.pow(u32_exp);
+    }
+
+    fn negative(&self) -> Self { -self }
+    fn pred(&self) -> Self { self - 1 }
+    fn succ(&self) -> Self { self + 1 }
+
+    fn from(source: BInteger) -> Self { source }
+    fn new(source: BInteger) -> Self { source }
+
+    fn isNatural(&self) -> BBoolean { return *self >= 0; }
+
+    fn isNotNatural(&self) -> BBoolean { return *self < 0; }
+
+    fn isNatural1(&self) -> BBoolean { return *self > 0; }
+
+    fn isNotNatural1(&self) -> BBoolean { return *self < 1; }
+}
+
+
+
+impl SetItem<INTEGER_SIZE> for BInteger {
+    fn as_idx(&self) -> usize {
+        if self < &LOWER_BOUND || self > &UPPER_BOUND {
+            panic!("Integer {} out of Integer bounds!", self);
+        }
+        return (self - LOWER_BOUND).try_into().unwrap();
+    }
+
+    fn from_idx(idx: usize) -> Self {
+        if idx > INTEGER_SIZE {
+            panic!("Integer-index {} is too large!", idx);
+        }
+        let bint_idx: BInteger = idx.try_into().unwrap();
+        return bint_idx + LOWER_BOUND;
+    }
+}
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/brelation.rs b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/brelation.rs
new file mode 100644
index 0000000000000000000000000000000000000000..3922a8a6e68a34cd7cc20ecef285d42f21d9e16d
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/brelation.rs
@@ -0,0 +1,636 @@
+#![ allow( non_snake_case) ]
+
+use core::convert::TryInto;
+use core::marker::PhantomData;
+use core::ops::{BitAnd, BitOrAssign};
+use bitvec::mem;
+use bitvec::array::BitArray;
+use bitvec::prelude::Lsb0;
+use crate::bboolean::BBoolean;
+use crate::binteger::{BInt, BInteger};
+use crate::bset::{BSet, PowSetItem, Set, SetItem};
+
+#[derive(Debug, Clone, Eq, PartialEq, Hash, PartialOrd, Ord)]
+pub struct BRelation<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize, const REL_SIZE: usize>
+where [usize; mem::elts::<usize>(LS*RS)]: Sized {
+    rel: BitArray<[usize; mem::elts::<usize>(LS*RS)], Lsb0>, // indexing: rel[l_idx*RS + r_idx]
+    _p: core::marker::PhantomData<L>,
+    _p2: core::marker::PhantomData<R>,
+}
+
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> Default for BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS>,
+      R: SetItem<RS>,
+      [usize; mem::elts::<usize>(LS*RS)]: Sized {
+    fn default() -> Self {
+        BRelation { rel: BitArray::ZERO, _p: PhantomData, _p2: PhantomData }
+    }
+}
+
+pub trait RelLeftItem<const LEFT_SIZE: usize, RightItem: SetItem<RIGHT_SIZE>, const RIGHT_SIZE: usize, const REL_VARIANTS: usize, const REL_SIZE: usize>: SetItem<LEFT_SIZE> {
+    type RelEnum: PowSetItem<REL_VARIANTS, REL_SIZE>;
+
+    fn rel_to_idx(rel_arr: [[bool; RIGHT_SIZE]; LEFT_SIZE]) -> usize {
+        let mut flat_arr = [false; REL_SIZE];
+        for left_idx in 0..LEFT_SIZE {
+            for right_idx in 0..RIGHT_SIZE {
+                flat_arr[left_idx * RIGHT_SIZE + right_idx] = rel_arr[left_idx][right_idx];
+            }
+        }
+        return Self::RelEnum::arr_to_idx(flat_arr);
+    }
+
+    fn idx_to_rel(idx: usize) -> [[bool; RIGHT_SIZE]; LEFT_SIZE] {
+        let flat_arr = Self::RelEnum::idx_to_arr(idx);
+        let mut result = [[false; RIGHT_SIZE]; LEFT_SIZE];
+        for left_idx in 0..LEFT_SIZE {
+            for right_idx in 0..RIGHT_SIZE {
+                result[left_idx][right_idx] = flat_arr[left_idx * RIGHT_SIZE + right_idx];
+            }
+        }
+        return result;
+    }
+}
+
+impl<L, const LS: usize, R, const RS: usize, const SIZE: usize, const REL_SIZE: usize> SetItem<SIZE> for BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS> + RelLeftItem<LS, R, RS, SIZE, REL_SIZE>,
+      R: SetItem<RS>,
+      [usize; mem::elts::<usize>(LS*RS)]: Sized {
+    fn as_idx(&self) -> usize {
+        let mut rel_arr: [[bool; RS]; LS] = [[false; RS]; LS];
+        for l_idx in 0..LS {
+            let left_idx = l_idx * RS;
+            for r_idx in 0..RS {
+                rel_arr[l_idx][r_idx] = self.rel[left_idx + r_idx];
+            }
+        }
+        return L::rel_to_idx(rel_arr);
+    }
+
+    fn from_idx(idx: usize) -> Self {
+        let mut res = BitArray::<[usize; mem::elts::<usize>(LS*RS)], Lsb0>::ZERO;
+        let rel_arr: [[bool; RS]; LS] = L::idx_to_rel(idx);
+        for l_idx in 0..LS {
+            let left_idx = l_idx * RS;
+            for r_idx in 0..RS {
+                res.set(left_idx + r_idx, rel_arr[l_idx][r_idx]);
+            }
+        }
+        return BRelation { rel: res, _p: PhantomData, _p2: PhantomData };
+    }
+}
+
+
+pub trait RelPowAble<const REL_VARIANTS: usize, const REL_SIZE: usize>: SetItem<REL_VARIANTS>
+where [usize; mem::elts::<usize>(REL_VARIANTS)]: Sized {
+    fn pow(&self) -> BSet<Self, REL_VARIANTS>;
+    fn pow1(&self) -> BSet<Self, REL_VARIANTS>;
+}
+
+impl<L, const LS: usize, R, const RS: usize, const SIZE: usize, const REL_SIZE: usize> RelPowAble<SIZE, REL_SIZE> for BRelation<L, LS, R, RS, REL_SIZE>
+    where L: SetItem<LS> + RelLeftItem<LS, R, RS, SIZE, REL_SIZE>,
+          R: SetItem<RS>,
+          [usize; mem::elts::<usize>(LS)]: Sized,
+          [usize; mem::elts::<usize>(RS)]: Sized,
+          [usize; mem::elts::<usize>(SIZE)]: Sized,
+          [usize; mem::elts::<usize>(LS*RS)]: Sized {
+    fn pow(&self) -> BSet<Self, SIZE> {
+        let mut result_arr = [false; SIZE];
+        for idx in 0..SIZE {
+            let crel = Self::from_idx(idx);
+            result_arr[idx] = crel.subset(&self);
+        }
+        return BSet::<Self, SIZE>::from_arr(result_arr);
+    }
+
+    fn pow1(&self) -> BSet<Self, SIZE> {
+        let mut result_arr = self.pow().as_arr();
+        let empty_self = Self::empty();
+        let empty_idx = empty_self.as_idx();
+        result_arr[empty_idx] = false;
+        return BSet::from_arr(result_arr);
+    }
+}
+
+
+
+pub trait TBRelation {
+    fn isPartialInteger(&self) -> BBoolean { false }
+    fn checkDomainInteger(&self) -> BBoolean { false }
+    fn isPartialNatural(&self) -> BBoolean { false }
+    fn checkDomainNatural(&self) -> BBoolean { false }
+    fn isPartialNatural1(&self) -> BBoolean { false }
+    fn checkDomainNatural1(&self) -> BBoolean { false }
+    fn checkRangeInteger(&self) -> BBoolean { false }
+    fn checkRangeNatural(&self) -> BBoolean { false }
+    fn checkRangeNatural1(&self) -> BBoolean { false }
+    fn checkDomainString(&self) -> BBoolean { false }
+    fn isPartialString(&self) -> BBoolean { false }
+    fn checkRangeString(&self) -> BBoolean { false }
+    fn checkDomainStruct(&self) -> BBoolean { false }
+    fn isPartialStruct(&self) -> BBoolean { false }
+    fn checkRangeStruct(&self) -> BBoolean { false }
+}
+
+impl<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize, const REL_SIZE: usize> TBRelation for BRelation<L, LS, R, RS, REL_SIZE>
+where [usize; mem::elts::<usize>(LS*RS)]: Sized {}
+
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
+    where L: SetItem<LS>,
+          R: SetItem<RS>,
+          [usize; mem::elts::<usize>(LS)]: Sized,
+          [usize; mem::elts::<usize>(RS)]: Sized,
+          [usize; mem::elts::<usize>(LS*RS)]: Sized {
+    
+    pub const fn empty() -> Self {
+        BRelation { rel: BitArray::ZERO, _p: PhantomData, _p2: PhantomData }
+    }
+    
+    pub const fn copy(&self) -> Self {
+        BRelation { rel: self.rel, _p: PhantomData, _p2: PhantomData }
+    }
+
+    pub fn slice_as_array(&self, left_idx: usize) -> [bool; RS] {
+        let l_idx = left_idx*RS;
+        let mut result = [false; RS];
+        for i in 0..RS { result[i] = self.rel[l_idx+i]; }
+        return result;
+    }
+
+    //TODO: pub fn iter(&self) -> BRelIter<L, LS, R, RS> { BRelIter::new(self.rel) }
+
+    pub fn _override_single(&self, left_item: L, right_item: R) -> Self {
+        let mut result = self.copy();
+        let left_idx = left_item.as_idx();
+        let right_idx = right_item.as_idx();
+        result.rel[left_idx*RS .. (left_idx*RS + RS-1)].fill(false);
+        result.rel.set(left_idx*RS + right_idx, true);
+        return result;
+    }
+
+    pub fn add_tuple(&mut self, left_item: &L, right_item: &R) {
+        //println!("adding tuple ({:?},{:?}), idx = [{}][{}]", left_item, right_item, left_item.as_idx(), right_item.as_idx());
+        self.rel.set(left_item.as_idx()*RS + right_item.as_idx(), true);
+    }
+
+    //b2program has this name hardcoded...
+    pub fn functionCall(&self, key: &L) -> R {
+        let l_idx = key.as_idx()*RS;
+        for i in 0..RS {
+            if self.rel[l_idx+i] { return R::from_idx(i) }
+        }
+        panic!("ERROR: key {:?} not found in set!", key);
+    }
+/*
+    pub fn fcall_to_set(&self, key: L) -> BSet<R, RS> {
+        let l_idx = key.as_idx()*RS;
+        let mut res = [false; RS];
+        for i in 0..RS {
+            res[i] = self.rel[l_idx+i];
+        }
+        return BSet::from_arr(res);
+    }
+*/
+    pub fn card(&self) -> BInteger {
+        return self.rel[0 .. RS*LS].count_ones().try_into().unwrap();
+    }
+
+    //this name is also hard-coded...
+    //checks if self.domain is a subset of the given set
+    pub fn checkDomain(&self, domain: &BSet<L, LS>) -> bool {
+        for left_idx in 0..LS {
+            if !domain.contains_idx(left_idx) && self.rel[left_idx * RS..(left_idx + 1) * RS].any() {
+                return false;
+            }
+        }
+        return true
+    }
+
+    pub fn isPartial(&self, domain: &BSet<L, LS>) -> bool { self.checkDomain(domain) }
+
+    pub fn isTotal(&self, domain: &BSet<L, LS>) -> bool {
+        for left_idx in 0..LS {
+            // self.domain.contains(left_idx) <=> domain.contains(left_idx)
+            if domain.contains_idx(left_idx) != self.rel[left_idx * RS..(left_idx + 1) * RS].any() {
+                return false;
+            }
+        }
+        return true
+    }
+
+    //this name is also hard-coded...
+    //checks if self.range is a subset of the given set
+    pub fn checkRange(&self, range: &BSet<R, RS>) -> bool {
+        let range_arr = range.as_bitarray();
+        for left_idx in 0..LS {
+            let current_range = &self.rel[left_idx * RS..(left_idx + 1) * RS];
+            if (range_arr & current_range) != current_range {
+                return false;
+            }
+        }
+        return true
+    }
+
+    //this name is also hard-coded...
+    //checks if for each L there is at most one R
+    pub fn isFunction(&self) -> bool {
+        for left_idx in 0..LS {
+            if self.rel[left_idx*RS .. (left_idx+1)*RS].count_ones() > 1 { return false; }
+        }
+        return true;
+    }
+
+    //checks f(x1) = f(x2) => x1 = x2
+    pub fn isInjection(&self) -> bool {
+        let mut checked = BitArray::<[usize; mem::elts::<usize>(RS)], Lsb0>::ZERO; //stores all the R's that were already 'used'
+        for i in 0..LS {
+            let current_slice = &self.rel[i*RS .. (i+1)*RS];
+            if checked.bitand(current_slice).any() { return false; } // one R of current slice is already in checked -> no injection
+            checked |= current_slice;
+        }
+        return true;
+    }
+
+    pub fn domain(&self) -> BSet<L, LS> {
+        let mut result = BitArray::<[usize; mem::elts::<usize>(LS)], Lsb0>::ZERO;
+        for i in 0..LS {
+            result.set(i, self.rel[i*RS .. (i+1)*RS].any());
+        }
+        return BSet::<L, LS>::from_bitarray(result);
+    }
+
+    pub fn range(&self) -> BSet<R, RS> {
+        let mut result = BitArray::<[usize; mem::elts::<usize>(RS)], Lsb0>::ZERO;
+        for left_idx in 0..LS {
+            result |= &self.rel[left_idx*RS .. (left_idx+1)*RS];
+        }
+        return BSet::<R, RS>::from_bitarray(result);
+    }
+
+    pub fn cartesian_product<TL, TR>(left_set: &TL, right_set: &TR) -> Self
+        where TL: Set<LS, ItemType = L>,
+              TR: Set<RS, ItemType = R> {
+        let right_arr = right_set.as_bitarray();
+        let mut bit_mask = BitArray::<[usize; mem::elts::<usize>(RS)], Lsb0>::ZERO;
+        let mut result = Self::empty();
+        for l_idx in 0..LS {
+            bit_mask.fill(left_set.contains_idx(l_idx));
+            result.rel[l_idx*RS .. (l_idx+1)*RS].copy_from_bitslice(&(right_arr & bit_mask));
+        }
+        return result;
+    }
+
+    pub fn inverse(&self) -> BRelation<R, RS, L, LS, REL_SIZE>
+    where [usize; mem::elts::<usize>(RS*LS)]: Sized {
+        let mut result = BRelation::<R, RS, L, LS, REL_SIZE>::empty();
+        for left_idx in 0..LS {
+            for right_idx in 0..RS {
+                result.rel.set(right_idx*LS + left_idx, self.rel[left_idx*RS + right_idx]);
+            }
+        }
+        return result;
+    }
+
+    pub fn domainRestriction(&self, domain_set: &BSet<L, LS>) -> Self {
+        let mut result = self.copy();
+        for left_idx in 0..LS {
+            if !domain_set.contains_idx(left_idx) { result.rel[left_idx*RS .. (left_idx+1)*RS].fill(false); }
+        }
+        return result;
+    }
+
+    pub fn domainSubstraction(&self, domain_set: &BSet<L, LS>) -> Self {
+        let mut result = self.copy();
+        for left_idx in 0..LS {
+            if domain_set.contains_idx(left_idx) { result.rel[left_idx*RS .. (left_idx+1)*RS].fill(false); }
+        }
+        return result;
+    }
+
+    pub fn rangeRestriction(&self, range_set: &BSet<R, RS>) -> Self {
+        let mut result = self.copy();
+        let range_arr = range_set.as_bitarray();
+        for left_idx in 0..LS {
+            //retain only elements that are in self *and* in range_set
+            result.rel[left_idx*RS .. (left_idx+1)*RS] &= range_arr;
+        }
+        return result;
+    }
+
+    pub fn rangeSubstraction(&self, range_set: &BSet<R, RS>) -> Self {
+        let mut result = self.copy();
+        let not_range_arr = !range_set.as_bitarray();
+        for left_idx in 0..LS {
+            //retain only elements that are in self *but not* in range_set
+            result.rel[left_idx*RS .. (left_idx+1)*RS] &= not_range_arr;
+        }
+        return result;
+    }
+
+    pub fn relationImage(&self, result_domain: &BSet<L, LS>) -> BSet<R, RS> {
+        let mut result_arr = BitArray::<[usize; mem::elts::<usize>(RS)], Lsb0>::ZERO;
+        for left_idx in 0..LS {
+            if result_domain.contains_idx(left_idx) {
+                result_arr.bitor_assign(&self.rel[left_idx*RS .. (left_idx+1)*RS]);
+            }
+        }
+        return BSet::<R, RS>::from_bitarray(result_arr);
+    }
+
+    pub fn intersect(&self, other: &Self) -> Self {
+        let mut result = self.copy();
+        result.rel &= other.rel;
+        return result;
+    }
+
+    pub fn difference(&self, other: &Self) -> Self {
+        let mut result = self.copy();
+        result.rel &= !other.rel;
+        return result;
+    }
+
+    pub fn union(&self, other: &Self) -> Self {
+        let mut result = self.copy();
+        result.rel |= other.rel;
+        return result;
+    }
+
+    pub fn equal(&self, other: &Self) -> BBoolean {
+        return self.rel.eq(&other.rel);
+    }
+
+    pub fn unequal(&self, other: &Self) -> BBoolean {
+        return !self.rel.eq(&other.rel);
+    }
+
+    pub fn elementOf(&self, (k, v): &(L, R)) -> BBoolean {
+        return self.rel[k.as_idx()*RS + v.as_idx()];
+    }
+
+    pub fn noElementOf(&self, (k, v): &(L, R)) -> BBoolean {
+        return !self.rel[k.as_idx()*RS + v.as_idx()];
+    }
+
+    //subset or equal
+    pub fn subset(&self, other: &Self) -> BBoolean {
+        return (other.rel & self.rel) == self.rel;
+    }
+
+    pub fn notSubset(&self, other: &Self) -> BBoolean {
+        return !self.subset(other);
+    }
+
+    pub fn _override(&self, other: &Self) -> Self {
+        let mut result = self.copy();
+        for left_idx in 0..LS {
+            let other_slice = &other.rel[left_idx*RS .. (left_idx+1)*RS];
+            if other_slice.any() { result.rel[left_idx*RS .. (left_idx+1)*RS].copy_from_bitslice(other_slice); }
+        }
+        return result;
+    }
+
+    //TODO: directProduct/ParallelProduct maybe?
+
+    pub fn composition<NewR, const NEW_RS: usize, const PARAM_TOTAL: usize, const NEW_TOTAL: usize>(&self, arg: &BRelation<R, RS, NewR, NEW_RS, PARAM_TOTAL>) -> BRelation<L, LS, NewR, NEW_RS, NEW_TOTAL>
+    where NewR: SetItem<NEW_RS>,
+          [usize; mem::elts::<usize>(NEW_RS)]: Sized,
+          [usize; mem::elts::<usize>(RS*NEW_RS)]: Sized,
+          [usize; mem::elts::<usize>(LS*NEW_RS)]: Sized {
+        let mut result = BRelation::<L, LS, NewR, NEW_RS, NEW_TOTAL>::empty();
+        for left_idx in 0..LS {
+            let l_idx = left_idx*NEW_RS;
+            //let mut foo: BitArray<[usize; mem::elts::<usize>(NEW_RS)], Lsb0> = BitArray::ZERO;
+            for r_idx in 0..RS {
+                if self.rel[l_idx+r_idx] { result.rel[l_idx .. l_idx+NEW_RS] |= &arg.rel[r_idx*NEW_RS .. (r_idx+1)*NEW_RS]; }
+            }
+            //result.rel[l_idx .. l_idx+NEW_RS].copy_from_bitslice(&foo);
+        }
+        return result;
+    }
+
+    //TODO: projection1/2 maybe? would need to impl SetItem for (L,R) and (R,L), might need adjustment in codegenerator?
+    //      or we use the relation-item enums for the tuples as well...
+    //BRelation<L,R> -> BRelation<L, BTuple<L, R>>
+    //BSet<BTuple<L, R>>
+
+    //TODO: support const-params in template? maybe compiler can figure them out itself?
+    pub fn fnc<NewR, const NEW_RS: usize, const NEW_REL_TOTAL: usize>(&self) -> BRelation<L, LS, NewR, NEW_RS, NEW_REL_TOTAL>
+    where NewR: Set<RS> + SetItem<NEW_RS>,                                  //BRelation<L, LS, BSet<R, RS>, NewRS, newRelTotal
+          [usize; mem::elts::<usize>(NEW_RS)]: Sized,
+          [usize; mem::elts::<usize>(LS*NEW_RS)]: Sized {
+        let mut result = BRelation::<L, LS, NewR, NEW_RS, NEW_REL_TOTAL>::empty();
+        for left_idx in 0..LS {
+            let result_set: [bool; RS] = self.slice_as_array(left_idx);
+            if !result_set.contains(&true) { continue; } // dont create mappings to empty set
+            result.rel.set(left_idx*LS + NewR::from_arr(result_set).as_idx(), true);
+        }
+        return result;
+    }
+
+    //pub fn nondeterminism(&self) -> (L, R) {
+    //    !todo!(RNG does not work without std/external crates)
+    //}
+
+    pub fn isTotalInteger(&self) -> BBoolean { return false; }
+    pub fn isTotalNatural(&self) -> BBoolean { return false; }
+    pub fn isTotalNatural1(&self) -> BBoolean { return false; }
+    pub fn isTotalString(&self) -> BBoolean { return false; }
+    pub fn isTotalStruct(&self) -> BBoolean { return false; }
+    pub fn isRelation(&self) -> BBoolean { return true;}
+    pub fn isSurjection(&self, range: &BSet<R, RS>) -> BBoolean { return self.range().equal(range); }
+    pub fn isSurjectionInteger(&self) -> BBoolean { return false; }
+    pub fn isSurjectionNatural(&self) -> BBoolean { return false; }
+    pub fn isSurjectionNatural1(&self) -> BBoolean { return false; }
+    pub fn isSurjectionString(&self) -> BBoolean { return false; }
+    pub fn isSurjectionStruct(&self) -> BBoolean { return false; }
+    pub fn isBijection(&self, range: &BSet<R, RS>) -> BBoolean { return self.isSurjection(range) && self.isInjection(); }
+    pub fn isBijectionInteger(&self) -> BBoolean { return false; }
+    pub fn isBijectionNatural(&self) -> BBoolean { return false; }
+    pub fn isBijectionNatural1(&self) -> BBoolean { return false; }
+    pub fn isBijectionString(&self) -> BBoolean { return false; }
+    pub fn isBijectionStruct(&self) -> BBoolean { return false; }
+}
+
+impl<L, const LS: usize, const REL_SIZE: usize> BRelation<L, LS, L, LS, REL_SIZE>
+where L: SetItem<LS>,
+      [usize; mem::elts::<usize>(LS)]: Sized,
+      [usize; mem::elts::<usize>(LS*LS)]: Sized {
+    pub fn identity(set: &BSet<L, LS>) -> Self {
+        let mut result = Self::empty();
+        for i in 0..LS {
+            if set.contains_idx(i) { result.rel.set(i*(LS+1), true); }
+        }
+        return result;
+    }
+
+    pub fn iterate(&self, n: &BInteger) -> Self {
+        return (0..*n).fold(BRelation::identity(&self.domain().union(&self.range())),
+                                     |rel, _| rel.composition(self));
+    }
+
+    pub fn closure(&self) -> Self { return self.closure_closure1(false); }
+
+    pub fn closure1(&self) -> Self { return self.closure_closure1(true); }
+
+    fn closure_closure1(&self, is_closure1: bool) -> Self {
+        let mut result = if is_closure1 { Self::empty() } else { self.iterate(&0) };
+        let mut current_iteration = self.iterate(&1);
+        let mut next_result = result.union(&current_iteration);
+        while !result.equal(&next_result) {
+            result = next_result;
+            current_iteration = current_iteration.composition(self);
+            next_result = result.union(&current_iteration);
+        }
+        return result;
+    }
+}
+
+//Sequence
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS> + BInt,
+      R: SetItem<RS>,
+      [usize; mem::elts::<usize>(LS)]: Sized,
+      [usize; mem::elts::<usize>(RS)]: Sized,
+      [usize; mem::elts::<usize>(LS*RS)]: Sized {
+
+    pub fn first(&self) -> R { self.functionCall(&L::from(1)) }
+    pub fn last(&self) -> R { self.functionCall(&L::from(self.card())) }
+    pub fn size(&self) -> BInteger { self.card() }
+
+    pub fn concat(&self, other: &Self) -> Self {
+        let mut result = self.copy();
+        let self_size = self.size();
+        for i in 1..=other.size() {
+            result.add_tuple(&L::from(self_size + i), &other.functionCall(&L::from(i)));
+        }
+        return result;
+    }
+
+    pub fn prepend(&self, e: &R) -> Self {
+        let mut result = Self::empty();
+        result.add_tuple(&L::from(1), e);
+        return result.concat(self);
+    }
+
+    pub fn append(&self, e: &R) -> Self {
+        let mut result = self.copy();
+        result.add_tuple(&L::from(self.size()+1), e);
+        return result;
+    }
+
+    pub fn reverse(&self) -> Self {
+        let mut result = Self::empty();
+        let self_size = self.size();
+        for i in 1..=self_size {
+            result.add_tuple(&L::from(i), &self.functionCall(&L::from(self_size - i + 1)))
+        }
+        return result;
+    }
+
+    pub fn front(&self) -> Self {
+        return self.take(&self.size().pred());
+    }
+
+    pub fn tail(&self) -> Self {
+        return self.drop(&1);
+    }
+
+    pub fn take(&self, n: &BInteger) -> Self {
+        let mut result = self.copy();
+        for i in (*n+1)..=self.size() {
+            let i_as_l = L::from(i);
+            result.rel.set(i_as_l.as_idx()*RS + self.functionCall(&i_as_l).as_idx(), false);
+        }
+        return result;
+    }
+
+    pub fn drop(&self, n: &BInteger) -> Self {
+        let mut result = Self::empty();
+        for i in (*n+1)..=self.size() {
+            result.add_tuple(&L::from(i-(*n)), &self.functionCall(&L::from(i)))
+        }
+        return result;
+    }
+
+    pub fn isPartialInteger(&self) -> BBoolean { true }
+    pub fn checkDomainInteger(&self) -> BBoolean { return self.isPartialInteger(); }
+    pub fn isPartialNatural(&self) -> BBoolean { return self.domain().subsetOfNatural(); }
+    pub fn checkDomainNatural(&self) -> BBoolean { return self.isPartialNatural(); }
+    pub fn isPartialNatural1(&self) -> BBoolean { return self.domain().subsetOfNatural1(); }
+    pub fn checkDomainNatural1(&self) -> BBoolean { return self.isPartialNatural1(); }
+}
+
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS>,
+      R: SetItem<RS> + BInt,
+      [usize; mem::elts::<usize>(LS)]: Sized,
+      [usize; mem::elts::<usize>(RS)]: Sized,
+      [usize; mem::elts::<usize>(LS*RS)]: Sized {
+    pub fn checkRangeInteger(&self) -> BBoolean { true }
+    pub fn checkRangeNatural(&self) -> BBoolean { return self.range().subsetOfNatural(); }
+    pub fn checkRangeNatural1(&self) -> BBoolean { return self.range().subsetOfNatural1(); }
+}
+
+
+pub struct BRelIter<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize> {
+    brel: [[bool; RS]; LS],
+    c_l: usize,
+    c_r: usize,
+    _p: PhantomData<L>,
+    _p2: PhantomData<R>,
+}
+
+impl<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize> BRelIter<L, LS, R, RS> {
+    pub const fn new(arr: [[bool; RS]; LS]) -> Self { BRelIter { brel: arr, c_l: 0, c_r: 0, _p: PhantomData, _p2: PhantomData } }
+}
+
+impl<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize> Iterator for BRelIter<L, LS, R, RS> {
+    type Item = (L, R);
+
+    fn next(&mut self) -> Option<Self::Item> {
+        while self.c_l < LS {
+            while self.c_r < RS {
+                if self.brel[self.c_l][self.c_r] {
+                    self.c_r += 1;
+                    return Option::Some((L::from_idx(self.c_l), R::from_idx(self.c_r-1)));
+                }
+                self.c_r += 1;
+            }
+            self.c_l += 1;
+            self.c_r = 0;
+        }
+        return Option::None;
+    }
+}
+
+
+/* // Does not work in stable rust
+impl<L, const LS: usize, R, const RS: usize, const TOTAL: usize, const INNER_RS: usize> BRelation<L, LS, R, RS, TOTAL>
+  where L: SetItem<LS>,
+        R: SetItem<RS> + Set<RS>,
+        R::ItemType: SetItem<INNER_RS>{
+    pub fn rel<const NEWSIZE: usize>(&self) -> BRelation<L, LS, R::ItemType, INNER_RS, NEWSIZE> {
+        let result = BRelation::<L, LS, R::ItemType, R::ItemType::VARIS, NEWSIZE>::empty();
+        return result;
+    }
+}
+*/
+/* //Needs SetItem on (L, R)/BTuple
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> Set<REL_SIZE> for BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS>,
+      R: SetItem<RS> {
+
+}
+*/
+#[macro_export]
+macro_rules! brel {
+    ($rel_type:ty $( ,$e:expr )* ) => {
+        {
+            let mut __temp_gen_rel__ = <$rel_type>::empty();
+            $(
+                __temp_gen_rel__.add_tuple(&$e.0, &$e.1);
+            )*
+            __temp_gen_rel__
+        }
+    };
+}
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/bset.rs b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/bset.rs
new file mode 100644
index 0000000000000000000000000000000000000000..0210c71bf7e9fa0e76a27990772358ed9524849c
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/bset.rs
@@ -0,0 +1,450 @@
+#![ allow( non_snake_case) ]
+
+use core::fmt::Debug;
+use core::marker::PhantomData;
+use bitvec::array::BitArray;
+use bitvec::mem;
+use bitvec::prelude::Lsb0;
+use crate::bboolean::BBoolean;
+use crate::binteger;
+use crate::binteger::{BInt, BInteger, set_BInteger};
+use crate::brelation::BRelation;
+
+/// Used to map an Enum to the position in a Set of it's type. \
+/// This is necessary since, even though a [BSet] is alway represented as a flat, 1D-array,
+/// we want to interact with the Set via more readable names, like the Enum itself. \
+/// Especially when it comes to nested sets, we need to be able to consistently convert the subsets
+/// into the corresponding array-index. This Trait, with its associated functions, allows us
+/// (and Rust) to make sure that such a conversion[^note] always exists and is consistent.
+///
+/// Ex.: Assume the EnumeratedSet `Counters = {C1, C2, C3}` \
+/// This will lead to the following enum in Rust (excerpt):
+/// ```rust
+/// pub enum Counters {
+///     C1 = 0,
+///     C2 = 1,
+///     C3 = 2,
+/// }
+/// impl SetItem<3> for Counters{/*...*/}
+/// type set_Counters = BSet<Counters, 3>;
+/// ```
+/// If we now create a set with that type, we can add elements to it simply by using these enums.
+/// ```rust
+/// let c: set_Counters = set_Counters::empty();
+/// c.add(Counters::C2);
+/// ```
+///
+/// [^note]: This conversion always goes in both directions, from enum to index and from index to enum.
+pub trait SetItem<const VARIANTS: usize>: Default + Debug {
+
+    /// Number of variations this SetItem has (i.e. size of the biggest set of this type)
+    const VARIANTS: usize = VARIANTS;
+
+    /// converts this SetItem into the index it corresponds to in any [BSet] of its type.
+    fn as_idx(&self) -> usize;
+
+    /// converts an index of any [BSet] of this SetItem's type into the SetItem. \
+    /// Note: this is the inverse to [SetItem::as_idx], `set_item = SetItem::from_idx(set_item.as_idx())`
+    fn from_idx(idx: usize) -> Self;
+}
+
+
+
+pub trait Set<const SIZE: usize>: Default {
+    type ItemType: SetItem<SIZE>;
+
+    fn as_arr(&self) -> [bool; SIZE];
+    fn as_bitarray(&self) -> BitArray<[usize; mem::elts::<usize>(SIZE)], Lsb0>;
+    fn from_arr(arr: [bool; SIZE]) -> Self;
+    fn contains_idx(&self, idx: usize) -> bool;
+    //checks if self is a subset of other
+    fn subset_of(&self, other: &Self) -> bool;
+
+}
+
+#[derive(Debug, Clone, Eq, PartialEq, Hash, PartialOrd, Ord)]
+pub struct BSet<I: SetItem<SIZE>, const SIZE: usize>
+where [usize; mem::elts::<usize>(SIZE)]: Sized {
+    arr: BitArray<[usize; mem::elts::<usize>(SIZE)], Lsb0>,
+    //arr: BitArray<[usize; {SIZE - 1}], Lsb0>,
+    _p: PhantomData<I>,
+}
+
+impl<I: SetItem<SIZE>, const SIZE: usize> Default for BSet<I, SIZE>
+where [usize; mem::elts::<usize>(SIZE)]: Sized {
+    fn default() -> Self { BSet { arr: BitArray::ZERO, _p: PhantomData } }
+}
+
+impl<I: SetItem<SIZE>, const SIZE: usize> Set<SIZE> for BSet<I, SIZE>
+where [usize; mem::elts::<usize>(SIZE)]: Sized {
+    type ItemType = I;
+    fn as_arr(&self) -> [bool; SIZE] {
+        let mut result = [false; SIZE];
+        for i in 0..SIZE { result[i] = self.arr[i]; }
+        return result;
+    }
+
+    fn as_bitarray(&self) -> BitArray<[usize; mem::elts::<usize>(SIZE)], Lsb0> { return self.arr.clone(); }
+    fn from_arr(arr: [bool; SIZE]) -> Self {
+        let mut bit_arr = BitArray::ZERO;
+        for i in 0..SIZE {
+            bit_arr.set(i, arr[i]);
+        }
+        return BSet { arr: bit_arr, _p: PhantomData };
+    }
+    fn contains_idx(&self, idx: usize) -> bool { self.arr[idx] }
+    fn subset_of(&self, other: &Self) -> bool {
+        return self.arr.eq(&(self.arr & other.arr));
+    }
+}
+
+/// Used to link the Enum-representation of a Set to the Enum-representation of it's subtype wich
+/// allows the use of [BSet]s as [SetItem]s.
+///
+/// In the generated code, we want to be able to use [BSet]s themselves as SetItems.
+/// This way, we can write `let some_set: BSet<BSet<Counters>>` which not only makes the type
+/// itself more readable, but any methods on `some_set` automatically use the 'correct' types. (i.e.
+/// iterating through the elements of `some_set` would automatically iterate through elements of type
+/// `BSet<Counters>`, instead of some enum-type.
+///
+/// To do this, [BSet] has to implement the [SetItem]-trait, which in turn requires an enum defining
+/// every possible variation of that Set. Unfortunately, we cannot implement that trait for the
+/// specific [BSet]s which need it during code-generation (Rust does not allow implementing external-traits
+/// for external structs). \
+/// However, we can implement the trait for [BSet] generically by defining some requirements that are
+/// needed for the implementation to work correctly. This requirement is the existence of an enum
+/// that fully represents the Set (i.e. carries one element for each possible SubSet). \
+/// That enum is then linked to the enum of it's subtype via this [PowSetItem]-trait, which the
+/// Rust-compiler can use to generate the specific impl's of the given Set (via the impl-definitions
+/// defined below).
+///
+/// todo(): example?
+///
+///
+/// SETVARIANTS-parameter is necessary to pass value along to SetItem-impl
+/// (caclulation on the fly is not possible (yet, generic_const_exprs is unstable/nightly)
+pub trait PowSetItem<const SETVARIANTS: usize, const ITEMVARIANTS: usize> {
+    //const SETVARIANTS: usize = SETVARIANTS;
+    //Implemented on top of SetItems, connects a SetItem to the Enum-representation of its Set
+    //SetRepr used to impl PowSetItem for BSet
+    type SetRepr: SetItem<SETVARIANTS>;
+    fn arr_to_idx(set_arr: [bool; ITEMVARIANTS]) -> usize;
+    fn idx_to_arr(idx: usize) -> [bool; ITEMVARIANTS];
+}
+
+impl<const SIZE: usize, const POWSIZE: usize, I> SetItem<POWSIZE> for BSet<I, SIZE>
+    where I: SetItem<SIZE> + PowSetItem<POWSIZE, SIZE>,
+          [usize; mem::elts::<usize>(SIZE)]: Sized {
+    fn as_idx(&self) -> usize { I::arr_to_idx(self.as_arr()) }
+    fn from_idx(idx: usize) -> Self { Self::from_arr(I::idx_to_arr(idx)) }
+}
+
+impl<const SETVARIANTS: usize, const ITEMVARIANTS: usize, const A: usize, I> PowSetItem<SETVARIANTS, ITEMVARIANTS> for BSet<I, A>
+    where I: SetItem<A> + PowSetItem<ITEMVARIANTS, A>,
+          I::SetRepr: SetItem<ITEMVARIANTS> + PowSetItem<SETVARIANTS, ITEMVARIANTS>,
+          [usize; mem::elts::<usize>(A)]: Sized  {
+    type SetRepr = <<I as PowSetItem<ITEMVARIANTS, A>>::SetRepr as PowSetItem<SETVARIANTS, ITEMVARIANTS>>::SetRepr;
+    fn arr_to_idx(set_arr: [bool; ITEMVARIANTS]) -> usize { I::SetRepr::arr_to_idx(set_arr) }
+    fn idx_to_arr(idx: usize) -> [bool; ITEMVARIANTS] { I::SetRepr::idx_to_arr(idx) }
+}
+
+pub trait PowAble<const SETLEN: usize, const ITEMVARS: usize>: Set<SETLEN> + SetItem<ITEMVARS>
+where [usize; mem::elts::<usize>(ITEMVARS)]: Sized{
+    fn pow(&self) -> BSet<Self, ITEMVARS>;
+    fn pow1(&self) -> BSet<Self, ITEMVARS>;
+    fn fin(&self) -> BSet<Self, ITEMVARS> { self.pow() }
+    fn fin1(&self) -> BSet<Self, ITEMVARS> { self.pow1() }
+}
+
+/// To generate the powerset of a BSet we need the corresponding enum already generated.
+/// This is the case if the BSet implements the [SetItem]-trait, so here we generically implement
+/// the pow-function for any struct that implements [Set] and [SetItem]
+/// (In theory, this would then automatically extend to BRelations as well, if we implement the traits there)
+impl<const SETLEN: usize, const ITEMVARS: usize , I> PowAble<SETLEN, ITEMVARS> for I
+    where I: Set<SETLEN> + SetItem<ITEMVARS>,
+    [usize; mem::elts::<usize>(ITEMVARS)]: Sized {
+
+    fn pow(&self) -> BSet<Self, ITEMVARS> {
+        let mut result = BSet::<Self, ITEMVARS>::empty();
+        for idx in 0..ITEMVARS {
+            let a = Self::from_idx(idx);
+            if a.subset_of(self) { result.arr.set(idx, true); }
+        }
+        return result;
+    }
+
+    fn pow1(&self) -> BSet<Self, ITEMVARS> {
+        let mut result = self.pow();
+        //remove empty set (usually, the index should always be 0, but this ensures that we get the correct one)
+        result.arr.set(Self::from_arr([false; SETLEN]).as_idx(), false);
+        return result;
+    }
+}
+
+
+impl<I: SetItem<SIZE>, const SIZE: usize> BSet<I, SIZE>
+where [usize; mem::elts::<usize>(SIZE)]: Sized  {
+    pub const fn empty() -> Self { BSet { arr: BitArray::ZERO, _p: PhantomData } }
+    pub const fn full() -> Self {
+        let mut res = Self::empty();
+        res.arr.data = [usize::MAX; mem::elts::<usize>(SIZE)];
+        return res;
+    }
+
+    pub fn from_bitarray(arr: BitArray<[usize; mem::elts::<usize>(SIZE)], Lsb0>) -> Self { BSet { arr, _p: PhantomData } }
+
+    pub const fn copy(&self) -> Self { BSet { arr: self.arr, _p: PhantomData } }
+    pub fn from_arr(arr: [bool; SIZE]) -> Self { <Self as Set<SIZE>>::from_arr(arr) }
+    pub fn iter(&self) -> BSetIter<I, SIZE> { BSetIter::new(self.as_arr()) } //TODO!
+    pub fn add(&mut self, element: I) { self.arr.set(element.as_idx(), true); }
+    pub fn add_idx(&mut self, idx: usize) { self.arr.set(idx, true); }
+
+    pub fn is_empty(&self) -> bool { self.arr.is_empty() }
+
+    pub fn equal(&self, other: &Self) -> BBoolean { self.arr.eq(&other.arr) }
+    pub fn unequal(&self, other: &Self) -> BBoolean { !self.arr.eq(&other.arr) }
+
+    pub fn card(&self) -> BInteger {
+        return self.arr.iter().fold(0,
+                             |size, next_item| if *next_item { size + 1 }
+                                                                 else { size });
+    }
+
+    pub fn subset(&self, other: &Self) -> BBoolean { self.subset_of(other) }
+    pub fn strictSubset(&self, other: &Self) -> BBoolean { self.card() < other.card() && self.subset_of(other) }
+    pub fn notSubset(&self, other: &Self) -> BBoolean { !self.subset_of(other) }
+    pub fn strictNotSubset(&self, other: &Self) -> BBoolean { self.card() >= other.card() || self.notSubset(other) }
+
+    pub fn union(&self, other: &Self) -> Self {
+        return BSet { arr: self.arr | other.arr, _p: PhantomData };
+    }
+
+    pub fn difference(&self, other: &Self) -> Self {
+        return BSet { arr: self.arr ^ (self.arr & other.arr), _p: PhantomData };
+    }
+
+    pub fn intersect(&self, other: &Self) -> Self {
+        return BSet { arr: self.arr & other.arr, _p: PhantomData };
+    }
+
+    //name hard-coded in b2program
+    pub fn elementOf(&self, element: &I) -> BBoolean { self.arr[element.as_idx()] }
+    pub fn notElementOf(&self, element: &I) -> BBoolean { !self.arr[element.as_idx()] }
+
+    //TODO: nondeterminism needs external libraries
+
+    pub fn interval(a: &BInteger, b: &BInteger) -> binteger::set_BInteger {
+        let mut result = set_BInteger::empty();
+        for idx in a.as_idx()..=b.as_idx() {
+            result.arr.set(idx, true);
+        }
+        return result;
+    }
+
+    pub const fn equalInteger(&self) -> BBoolean { false }
+
+    pub const fn unequalInteger(&self) -> BBoolean { true }
+
+    pub const fn equalNatural(&self) -> BBoolean { false }
+
+    pub const fn unequalNatural(&self) -> BBoolean { true }
+
+    pub const fn equalNatural1(&self) -> BBoolean { false }
+
+    pub const fn unequalNatural1(&self) -> BBoolean { true }
+
+    pub const fn equalString(&self) -> BBoolean { false }
+
+    pub const fn unequalString(&self) -> BBoolean { true }
+
+    pub const fn equalStruct(&self) -> BBoolean { false }
+
+    pub const fn unequalStruct(&self) -> BBoolean { true }
+
+    pub const fn subsetOfString(&self) -> BBoolean { false } //TODO?
+
+    pub const fn strictSubsetOfString(&self) -> BBoolean { return self.subsetOfString(); }
+
+    pub const fn notSubsetOfString(&self) -> BBoolean { return !self.subsetOfString(); }
+
+    pub const fn notStrictSubsetOfString(&self) -> BBoolean { return !self.strictSubsetOfString(); }
+
+    pub const fn subsetOfStruct(&self) -> BBoolean { false } //TODO?
+
+    pub const fn strictsubsetOfStruct(&self) -> BBoolean { return self.subsetOfStruct(); }
+
+    pub const fn notsubsetOfStruct(&self) -> BBoolean { return !self.subsetOfStruct(); }
+
+    pub const fn notStrictsubsetOfStruct(&self) -> BBoolean { return !self.strictsubsetOfStruct(); }
+
+    //equals BRelation.checkDomain(BSet)
+    pub fn check_domain_of<R, const RS: usize, const TOTAL_REL: usize>(&self, of: &BRelation<I, SIZE, R, RS, TOTAL_REL>) -> BBoolean
+    where R: SetItem<RS>,
+          [usize; mem::elts::<usize>(RS)]: Sized,
+          [usize; mem::elts::<usize>(SIZE*RS)]: Sized {
+        return self.is_superset(&of.domain());
+    }
+
+    //equals BRelation.checkRange(BSet)
+    pub fn check_range_of<L, const LS: usize, const TOTAL_REL: usize>(&self, of: &BRelation<L, LS, I, SIZE, TOTAL_REL>) -> BBoolean
+        where L: SetItem<LS>,
+              [usize; mem::elts::<usize>(LS)]: Sized,
+              [usize; mem::elts::<usize>(LS*SIZE)]: Sized {
+        return self.is_superset(&of.range());
+    }
+
+    pub fn check_partial_of<R: SetItem<RS>, const RS: usize, const TOTAL_REL: usize>(&self, of: &BRelation<I, SIZE, R, RS, TOTAL_REL>) -> BBoolean
+        where R: SetItem<RS>,
+              [usize; mem::elts::<usize>(RS)]: Sized,
+              [usize; mem::elts::<usize>(SIZE*RS)]: Sized {
+        return self.is_superset(&of.domain());
+    }
+
+    pub fn is_superset(&self, other: &Self) -> BBoolean { return other.subset(self); }
+
+    pub fn check_total_of<R: SetItem<RS>, const RS: usize, const TOTAL_REL: usize>(&self, of: &BRelation<I, SIZE, R, RS, TOTAL_REL>) -> BBoolean
+        where R: SetItem<RS>,
+              [usize; mem::elts::<usize>(RS)]: Sized,
+              [usize; mem::elts::<usize>(SIZE*RS)]: Sized {
+        return self.equal(&of.domain());
+    }
+}
+
+impl <I: SetItem<SIZE> + BInt, const SIZE: usize> BSet<I, SIZE>
+where [usize; mem::elts::<usize>(SIZE)]: Sized  {
+
+    pub const fn subsetOfInteger(&self) -> BBoolean { true }
+
+    pub const fn notSubsetOfInteger(&self) -> BBoolean { !self.subsetOfInteger() }
+
+    pub const fn strictSubsetOfInteger(&self) -> BBoolean { self.subsetOfInteger() }
+
+    pub fn notStrictSubsetOfInteger(&self) -> BBoolean { !self.strictSubsetOfInteger() }
+
+    pub fn subsetOfNatural(&self) -> BBoolean {
+        if binteger::LOWER_BOUND < 0 { // if LB >= 0, every Int-set only holds Integers >= 0
+            for idx in 0..BInteger::as_idx(&0) {
+                if self.arr[idx] { return false; }
+            }
+        }
+        return true;
+    }
+
+    pub fn notSubsetOfNatural(&self) -> BBoolean { !self.subsetOfNatural() }
+
+    pub fn strictSubsetOfNatural(&self) -> BBoolean { self.subsetOfNatural() }
+
+    pub fn notStrictSubsetOfNatural(&self) -> BBoolean { self.strictSubsetOfNatural() }
+
+    pub fn subsetOfNatural1(&self) -> BBoolean {
+        if binteger::LOWER_BOUND < 1 {
+            for idx in 0..BInteger::as_idx(&1) {
+                if self.arr[idx] { return false; }
+            }
+        }
+        // we could also do self.min() > 0, but that might be slower
+        return true;
+    }
+
+    pub fn notSubsetOfNatural1(&self) -> BBoolean { !self.subsetOfNatural1() }
+
+    pub fn strictSubsetOfNatural1(&self) -> BBoolean { self.subsetOfNatural() }
+
+    pub fn notStrictSubsetOfNatural1(&self) -> BBoolean { !self.strictSubsetOfNatural1() }
+
+    pub fn _min(&self) -> BInteger {
+        for idx in 0..SIZE {
+            if self.arr[idx] { return BInteger::from_idx(idx); }
+        }
+        panic!("Called min on empty Set!");
+    }
+
+    pub fn _max(&self) -> BInteger {
+        for idx in (0..SIZE).rev() {
+            if self.arr[idx] { return BInteger::from_idx(idx); }
+        }
+        panic!("Called max on empty Set!");
+    }
+}
+
+/*
+EINT: SetItem<4> + PowSetItem<16, 4>
+BSet<EINT, 4>: Set<4> + SetItem<16>
+BSet<BSet<Enit, 4>, 16>: Set<16>
+*/
+
+pub trait NestedSet<const OUTER_SIZE: usize, const INNER_SIZE: usize>
+where Self: Set<OUTER_SIZE>,
+      Self::ItemType: Set<INNER_SIZE> + SetItem<OUTER_SIZE> {
+
+    fn unary_union(&self) -> Self::ItemType { self.unary_combine(|l, r| l || r) }
+    fn unary_intersect(&self) -> Self::ItemType { self.unary_combine(|l, r| l && r) }
+    fn unary_combine(&self, comb_fn: fn(left_bool:bool, right_bool: bool) -> bool) -> Self::ItemType;
+}
+
+/// Implements functions for nested-Sets.
+/// A nested-Set is still just a 1D-array, but the Set-Item implements the Set-trait,
+/// so the index can be converted to another 1D-array (this then being the representation of the inners Sets)
+///
+/// Because Rust is a bit constrained in how these implementations can be defined, we need to use
+/// a trait to define how the specific Set should look, and then implement that trait generically for
+/// any I that conforms to further constrictions.
+/// (This will ulitmately only apply to BSets where the inner-type is also a BSet.)
+impl<const OUTER_SIZE: usize, const INNER_SIZE: usize, I> NestedSet<OUTER_SIZE, INNER_SIZE> for I
+where I: Set<OUTER_SIZE>,
+      I::ItemType: Set<INNER_SIZE> + SetItem<OUTER_SIZE>{
+
+    fn unary_combine(&self, comb_fn: fn(left_bool:bool, right_bool: bool) -> bool) -> I::ItemType {
+        let mut result_arr = [false; INNER_SIZE]; // empty array representation of the inner settype
+        for outer_idx in 0..OUTER_SIZE {
+            if self.contains_idx(outer_idx) {
+                let inner_set_arr = I::ItemType::from_idx(outer_idx).as_arr(); // array representation of the current inner-set
+                for inner_idx in 0..INNER_SIZE { result_arr[inner_idx] = comb_fn(result_arr[inner_idx], inner_set_arr[inner_idx]); } // logical combination between the arrays (or = union; and = intersection between sets)
+            }
+        }
+        return I::ItemType::from_arr(result_arr);
+    }
+}
+
+pub struct BSetIter<I: SetItem<SIZE>, const SIZE: usize> {
+    bset: [bool; SIZE],
+    c: usize,
+    _p: PhantomData<I>,
+}
+
+impl<I: SetItem<SIZE>, const SIZE: usize> BSetIter<I, SIZE> {
+    pub const fn new(arr: [bool; SIZE]) -> Self { BSetIter { bset: arr, c: 0, _p: PhantomData } }
+}
+
+impl<I: SetItem<SIZE>, const SIZE: usize> Iterator for BSetIter<I, SIZE> {
+    type Item = I;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        while self.c < SIZE {
+            if self.bset[self.c] {
+                self.c += 1;
+                return Option::Some(I::from_idx(self.c-1));
+            }
+            self.c += 1;
+        }
+        return Option::None;
+    }
+}
+
+/// Macro to simplify the creation of [Bset]s.
+/// Originally, this was supposed to only use constant expressions, so that
+/// these could be evaluated at compile-time. However, in rust it is currently
+/// not possible to define trait-functions as const, which would be necessary to make this
+/// work generically.
+#[macro_export]
+macro_rules! bset {
+    ($set_type:ty$(, $e:expr )* ) => {
+        {
+            let mut __temp_gen_arr__ = [false; <$set_type>::VARIANTS];
+            $(
+                __temp_gen_arr__[($e).as_idx()] = true;
+            )*
+            BSet::<$set_type, { <$set_type>::VARIANTS }>::from_arr(__temp_gen_arr__)
+        }
+    };
+}
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/btuple.rs b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/btuple.rs
new file mode 100644
index 0000000000000000000000000000000000000000..611f77f16b53bd7d894a87506816e22329cf0471
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/btuple.rs
@@ -0,0 +1,15 @@
+
+
+pub trait BTuple<L, R> {
+    fn projection1(self) -> L;
+    fn projection2(self) -> R;
+}
+
+impl<L, R> BTuple<L, R> for (L, R)
+where L: Clone,
+      R: Clone {
+    fn projection1(self) -> L { self.0.clone() }
+    fn projection2(self) -> R { self.1.clone() }
+}
+
+//TODO: Somehow impl SetItem
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/lib.rs b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/lib.rs
new file mode 100644
index 0000000000000000000000000000000000000000..00af4824f8aebf0bf4048f8b3c0c4e2eba597d54
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes_bitvec/src/lib.rs
@@ -0,0 +1,16 @@
+#![no_std]
+#![feature(generic_const_exprs)]
+#[macro_use]
+//extern crate lazy_static;
+
+pub mod bboolean;
+pub mod binteger;
+//pub mod bobject;
+//pub mod bstruct;
+pub mod bset;
+//pub mod bstring;
+pub mod btuple;
+pub mod brelation;
+//pub mod butils;
+//pub mod orderedhashset;
+//pub mod set;
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java
index e663523b57774366627e5d486772dc7825d861ce..e88eb192fbfa86df769a586b33a785e6a9f3cb0f 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java
@@ -22,12 +22,20 @@ import static org.junit.Assert.*;
 
 public class TestRSE {
     final ClassLoader classLoader = this.getClass().getClassLoader();
-    final Path tomlPath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml"));
-    final Path tomlPath_MC = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml"));
-    final Path rustSrcPath = tomlPath.getParent().resolve(Paths.get("src/"));
+    //array
+    //final Path tomlPath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml"));
+    //bitvec
+    final Path tomlPath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml"));
+    //final Path tomlPath_MC = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml"));
+    final Path tomlPath_MC = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml"));
+    //final Path rustSrcPath = tomlPath.getParent().resolve(Paths.get("src/")); // arrays
+    final Path rustSrcPath = tomlPath.getParent().resolve(Paths.get("src/")); // bitvec
+    //final Path rustSrcPath_MC = tomlPath_MC.getParent().resolve(Paths.get("src/"));
     final Path rustSrcPath_MC = tomlPath_MC.getParent().resolve(Paths.get("src/"));
     final Runtime runtime = Runtime.getRuntime();
     final Path testFileBasePath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().resolve("resources/test/de/hhu/stups/codegenerator/");
+    //final String cargoChannel = "";
+    final String cargoChannel = "+nightly";
 
     public TestRSE() throws URISyntaxException, IOException {
         Files.createDirectories(rustSrcPath);
@@ -58,7 +66,7 @@ public class TestRSE {
 
     public void compileTestFiles(boolean forModelChecking) throws IOException, InterruptedException {
         Path usedTomlPath = !forModelChecking ? tomlPath : tomlPath_MC;
-        Process process = runtime.exec("cargo build --release --manifest-path " + usedTomlPath);
+        Process process = runtime.exec(String.format("cargo %s build --release --manifest-path %s", cargoChannel, usedTomlPath));
         TestHelper.writeInputToSystem(process.getErrorStream());
         TestHelper.writeInputToOutput(process.getErrorStream(), process.getOutputStream());
         process.waitFor();
@@ -75,7 +83,7 @@ public class TestRSE {
 
         Path usedTomlPath = !modelChecking ? tomlPath : tomlPath_MC;
 
-        Process executeProcess = runtime.exec("cargo run --release --manifest-path " + usedTomlPath + progArgs);
+        Process executeProcess = runtime.exec(String.format("cargo %s run --release --manifest-path %s %s", cargoChannel, usedTomlPath, progArgs));
         executeProcess.waitFor();
 
         String error = TestHelper.streamToString(executeProcess.getErrorStream());