Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision e49c308e3a7e1d9cdf4521ccf7d8491c411451fe)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision f6bbc92044afb0bdffb4c86566e1b3401e2c5196)
@@ -204,8 +204,16 @@
 enum( char ) Letter { A = 'A', ... };
 enum( @Letter@ ) Greek { Alph = A, Beta = B, ... }; // alphabet intersection
-\end{cfa}
-Enumeration @Greek@ may have more or less enums than @Letter@, but the enum values \emph{must} be from @Letter@.
-Therefore, @Greek@ enums are a subset of type @Letter@ and are type compatible with enumeration @Letter@, but @Letter@ enums are not type compatible with enumeration @Greek@.
-
+
+void foo(Letter l);
+foo(Beta);			$\C{// foo(value(Beta))}$
+\end{cfa}
+Enumeration @Greek@ may have more or less enumerators than @Letter@, but the enum values \emph{must} be of a member of @Letter@.
+Therefore, the set of @Greek@ enum value in a subset of the value set of type @Letter@. 
+@Letter@ is type compatible with enumeration @Letter@ thanks to \CFA inserts value conversion whenever @Letter@ be used 
+in place of @Greek@. On the other hand, @Letter@ enums are not type compatible with enumeration @Greek@.
+As a result, @Greek@ becomes a logical subtype of @Letter@.
+
+Subset defines an implicit subtyping relationship between two \CFA enumerations. \CFA also has 
+containment inheritance for \CFA enumerations where subtyping is explicitly structured.
 
 \section{Inheritance}
@@ -236,60 +244,26 @@
 However, the position of the underlying representation is the order of the enumerator in the new enumeration.
 \begin{cfa}
-enum() E1 { A };
-enum() E2 { B, C };
-enum() E3 { inline E1, inline E2, D };
-\end{cfa}
-Here, @A@ has position 0 in @E1@ and @E3@.
-@B@ has position 0 in @E2@ and 1 in @E3@.
-@C@ has position 1 in @E2@ and position 2 in @E3@.
-@D@ has position 3 in @E3@.
-
-A subtype enumeration can be casted, or implicitly converted into its supertype, with a @safe@ cost.
+enum() E1 { B };								$\C{// B}$						
+enum() E2 { C, D };								$\C{// C D}$
+enum() E3 { inline E1, inline E2, E };			$\C{// {\color{red}[\(_{E1}\)} B {\color{red}]} {\color{red}[\(_{E2}\)} C D {\color{red}]} E}$
+enum() E4 { A, inline E3, F};					$\C{// A {\color{blue}[\(_{E3}\)} {\color{red}[\(_{E1}\)} B {\color{red}]} {\color{red}[\(_{E2}\)} C D {\color{red}]} E {\color{blue}]} F }$
+\end{cfa}
+In the example above, @B@ has the position 0 in @E1@ and @E3@, but it at the position 1 in @E4@ as @A@ taking the 0 in @E4@.
+@C@ is at the position 0 in @E2@, 1 in @E3@ and 2 in E4. @D@ is at the position 1 in @E2@, 2 in @E3@ and 3 in @E4@. 
+
+A subtype enumeration can be casted, or implicitly converted into its supertype, with a @safe@ cost. Such conversion is an @enumeration conversion@. 
 \begin{cfa}
 enum E2 e2 = C;
-posn( e2 );			$\C[1.75in]{// 1}$
+posn( e2 );			$\C[1.75in]{// 0}$
 enum E3 e3 = e2;
-posn( e2 );			$\C{// 2}$
+posn( e2 );			$\C{// 1}$
 void foo( E3 e );
 foo( e2 );
-posn( (E3)e2 );		$\C{// 2}$
+posn( (E3)e2 );		$\C{// 1}$
 E3 e31 = B;
-posn( e31 );		$\C{// 1}\CRT$
+posn( e31 );		$\C{// 0}\CRT$
 \end{cfa}
 The last expression is unambiguous.
 While both @E2.B@ and @E3.B@ are valid candidate, @E2.B@ has an associated safe cost and \CFA selects the zero cost candidate @E3.B@.
-Hence, as discussed in \VRef{s:OpaqueEnum}, \CFA chooses position as a representation of the \CFA enum.
-Therefore, conversion involves both a change of type and possibly position.
-
-When converting a subtype to a supertype, its position can only be a larger value.
-The difference between the position in the subtype and in the supertype is its \newterm{offset}.
-\VRef[Figure]{s:OffsetSubtypeSuperType} show the algorithm to determine the offset for an subtype enumerator to its super type.
-\PAB{You need to explain the algorithm.}
-
-\begin{figure}
-\begin{cfa}
-struct Enumerator;
-struct CFAEnum {
-	vector<variant<CFAEnum, Enumerator>> members;
-};
-pair<bool, int> calculateEnumOffset( CFAEnum dst, Enumerator e ) {
-	int offset = 0;
-	for ( auto v: dst.members ) {
-		if ( v.holds_alternative<Enumerator>() ) {
-			auto m = v.get<Enumerator>();
-			if ( m == e ) return make_pair( true, 0 );
-			offset++;
-		} else {
-			auto p = calculateEnumOffset( v, e );
-			if ( p.first ) return make_pair( true, offset + p.second );
-			offset += p.second;
-		}
-	}
-	return make_pair( false, offset );
-}
-\end{cfa}
-\caption{Compute Offset from Subtype Enumerator to Super Type}
-\label{s:OffsetSubtypeSuperType}
-\end{figure}
 
 For the given function prototypes, the following calls are valid.
@@ -313,4 +287,53 @@
 Note, the validity of calls is the same for call-by-reference as for call-by-value, and @const@ restrictions are the same as for other types.
 
+\subsection{Offset Calculation}
+As discussed in \VRef{s:OpaqueEnum}, \CFA chooses position as a representation of a \CFA enumeration variable.
+Because enumerators has different @position@ between subtype and supertype, \CFA might need to manipulate the representation whenever a cast or 
+implicit conversion involves two \CFA enums. \CFA determine how a position is going to change with an @offset calculation@ function, reflects to 
+enumerator as an arithmetic expression. Casting an enumeration of subtype to a supertype, the position can be unchanged or increase. The change 
+of position is an @offset@.  
+
+\begin{figure}
+\begin{cfa}
+struct Enumerator;
+struct CFAEnum { vector<variant<CFAEnum, Enumerator>> members; string name; };
+inline static bool operator==(CFAEnum& lhs, CFAEnum& rhs) { return lhs.name == rhs.name; }
+pair<bool, int> calculateEnumOffset(CFAEnum src, CFAEnum dst) {
+	int offset = 0;
+	if (src == dst) return make_pair(true, 0);
+	for (auto v : dst.members) {
+		if (holds_alternative<Enumerator>(v)) {
+			offset++;
+		} else {
+			auto m = get<CFAEnum>(v);
+			if (m == src) return make_pair(true, offset);
+			auto dist = calculateEnumOffset(src, m);
+			if (dist.first) {
+				return make_pair(true, offset + dist.second);
+			} else {
+				offset += dist.second;
+			}
+		}
+	}
+	return make_pair(false, offset);
+}
+\end{cfa}
+\caption{Compute Offset from Subtype Enumeration to a Supertype}
+\label{s:OffsetSubtypeSuperType}
+\end{figure}
+
+Figure~\ref{s:OffsetSubtypeSuperType} shows a minimum of @offset calculation@, written in \CC. CFAEnum represents \CFA enumeration 
+which has a vector of variants of Enumerator or CFAEnum. Two CFAEnums are differentiable by their unquie name.
+The algorithm takes two CFAEnums as parameters @src@ and @dst@, with @src@ being type of expression the conversion applies on, 
+and @dst@ being type that the expression cast into. The algorithm returns a pair of value: when @src@ is convertible to @dst@ (@src@ is a subtype of @dst@),
+it returns boolean true and the offset. Otherwise, it returns false and the size of @src@ (total number of enumerators in @src@). The offset between a type and itself is defined 
+as 0. 
+
+The algorithm iterates over members in @dst@ to find @src@. If a member is an enumerator of @dst@, the positions of all subsequent members
+increment by one. If the current member is @dst@, the function returns true indicating "found" and the accumulated offset. Otherwise, the algorithm recurse 
+into the current CFAEnum @m@ and find out if the @src@ is convertible to @m@. The @src@ being convertible to the current member @m@ means @src@ 
+is a "subtype of subtype" of @dst@. The offset between @src@ and @dst@ is the sum of the offset of @m@ in @dst@ and the offset of 
+@src@ in @m@. If @src@ is not a subtype of @m@, the loop continue but with offset shifted by the size of @m@. The procedure reaches the end 
+of the loop proves @src@ is not convertible to @dst@. It returns size of @src@ in case it is in a recurse innvocation and size is needed for offset update. 
 
 \section{Control Structures}
Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision e49c308e3a7e1d9cdf4521ccf7d8491c411451fe)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision f6bbc92044afb0bdffb4c86566e1b3401e2c5196)
@@ -487,4 +487,4 @@
 
 In \CFA, the meaning of a C style cast is determined by its @Cast Cost@. For most cast expression resolution, a cast cost is equal to a conversion cost.
-Cast cost exists as an independent matrix for conversion that cannot happen implcitly, while being possible with an explicit cast. These conversions are often defined to have
+Cast cost exists as an independent matrix for conversion that cannot happen implicitly, while being possible with an explicit cast. These conversions are often defined to have
 infinite conversion cost and non-infinite cast cost.
Index: src/Validate/ImplementEnumFunc.cpp
===================================================================
--- src/Validate/ImplementEnumFunc.cpp	(revision e49c308e3a7e1d9cdf4521ccf7d8491c411451fe)
+++ src/Validate/ImplementEnumFunc.cpp	(revision f6bbc92044afb0bdffb4c86566e1b3401e2c5196)
@@ -210,8 +210,5 @@
 		"value",
 		{new ast::ObjectDecl(getLocation(), "_i", new ast::EnumInstType(decl))},
-		{new ast::ObjectDecl(getLocation(), "_ret",
-							ast::deepCopy(decl->base))});
-	// else
-	// 	return genQuasiValueProto();
+		{new ast::ObjectDecl(getLocation(), "_ret", decl->base)});
 }
 
