	public IProofObligationList caseAExplicitFunctionDefinition(
			AExplicitFunctionDefinition node, IPOContextStack question)
			throws AnalysisException
	{
		try
		{
			if (node.getBody() instanceof ANotYetSpecifiedExp)
			{
				return new ProofObligationList();
			}
			IProofObligationList obligations = new ProofObligationList();
			LexNameList pids = new LexNameList();
			AFunctionType ftype = (AFunctionType) node.getType();
			boolean alwaysMatches = true;
			for (List<PPattern> params : node.getParamPatternList())
			{
				alwaysMatches = params.isEmpty() && alwaysMatches;
			}
			if (alwaysMatches)
			{
			} else
			{
				alwaysMatches = false;
				PatternAlwaysMatchesVisitor amVisitor = new PatternAlwaysMatchesVisitor();
				for (List<PPattern> patterns : node.getParamPatternList())
					for (PPattern p : patterns)
					{
						for (PDefinition def : p.getDefinitions())
							pids.add(def.getName());
						alwaysMatches = alwaysMatches && p.apply(amVisitor);
					}
			}
			if (pids.hasDuplicates() || !alwaysMatches)
			{
				obligations.add(new ParameterPatternObligation(node, question));
			}
			PExp precondition = node.getPrecondition();
			if (precondition != null)
			{
				question.push(new POFunctionDefinitionContext(node, false));
				obligations.addAll(precondition.apply(rootVisitor, question));
				question.pop();
			}
			PExp postcondition = node.getPostcondition();
			if (postcondition != null)
			{
				question.push(new POFunctionDefinitionContext(node, false));
				obligations.add(new FuncPostConditionObligation(node, question));
				question.push(new POFunctionResultContext(node));
				obligations.addAll(postcondition.apply(rootVisitor, question));
				question.pop();
				question.pop();
			}
			question.push(new POFunctionDefinitionContext(node, true));
			PExp body = node.getBody();
			int sizeBefore = question.size();
			obligations.addAll(body.apply(rootVisitor, question));
			assert sizeBefore <= question.size();
			if (node.getIsUndefined()
					|| !TypeComparator.isSubType(node.getActualResult(), node.getExpectedResult()))
			{
				SubTypeObligation sto = SubTypeObligation.newInstance(node, node.getExpectedResult(), node.getActualResult(), question);
				if (sto != null)
				{
					obligations.add(sto);
				}
			}
			question.pop();
			return obligations;
		} catch (Exception e)
		{
			throw new POException(node, e.getMessage());
		}
	}

	public IProofObligationList caseAExplicitFunctionDefinition(
			AExplicitFunctionDefinition node, IPOContextStack question)
			throws AnalysisException
	{
		try
		{
			if (node.getBody() instanceof ANotYetSpecifiedExp)
			{
				return new ProofObligationList();
			}
			IProofObligationList obligations = new ProofObligationList();
			LexNameList pids = new LexNameList();
			AFunctionType ftype = (AFunctionType) node.getType();
			boolean alwaysMatches = true;
			for (List<PPattern> params : node.getParamPatternList())
			{
				alwaysMatches = params.isEmpty() && alwaysMatches;
			}
			if (alwaysMatches)
			{
			} else
			{
				alwaysMatches = true;
				PatternAlwaysMatchesVisitor amVisitor = new PatternAlwaysMatchesVisitor();
				for (List<PPattern> patterns : node.getParamPatternList())
					for (PPattern p : patterns)
					{
						for (PDefinition def : p.getDefinitions())
							pids.add(def.getName());
						alwaysMatches = alwaysMatches && p.apply(amVisitor);
					}
			}
			if (pids.hasDuplicates() || !alwaysMatches)
			{
				obligations.add(new ParameterPatternObligation(node, question));
			}
			PExp precondition = node.getPrecondition();
			if (precondition != null)
			{
				question.push(new POFunctionDefinitionContext(node, false));
				obligations.addAll(precondition.apply(rootVisitor, question));
				question.pop();
			}
			PExp postcondition = node.getPostcondition();
			if (postcondition != null)
			{
				question.push(new POFunctionDefinitionContext(node, false));
				obligations.add(new FuncPostConditionObligation(node, question));
				question.push(new POFunctionResultContext(node));
				obligations.addAll(postcondition.apply(rootVisitor, question));
				question.pop();
				question.pop();
			}
			question.push(new POFunctionDefinitionContext(node, true));
			PExp body = node.getBody();
			int sizeBefore = question.size();
			obligations.addAll(body.apply(rootVisitor, question));
			assert sizeBefore <= question.size();
			if (node.getIsUndefined()
					|| !TypeComparator.isSubType(node.getActualResult(), node.getExpectedResult()))
			{
				SubTypeObligation sto = SubTypeObligation.newInstance(node, node.getExpectedResult(), node.getActualResult(), question);
				if (sto != null)
				{
					obligations.add(sto);
				}
			}
			question.pop();
			return obligations;
		} catch (Exception e)
		{
			throw new POException(node, e.getMessage());
		}
	}
