Error Number: 129

Mizar Message:

Invalid free variables in a Fraenkel operator

Description

Often happens if the types of variables ("LambdaVariables") parameterizing the Fraenkel term do not widen to the type "Element of X" where X is non empty set. The non emptiness requirement seems a bit redundant, see FraenkelNonEmpty.

-- JosefUrban - 25 Jul 2002

To use a Fraekel term, you need:

• The directive: requirements SUBSET;
• Fraenkel variables that widen to type: Element of X

Example

environ

 notations TARSKI, NUMBERS;
 constructors TARSKI, NUMBERS;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM;

 notations NAT_1;
 constructors NAT_1;

begin

    reserve k for Nat;
    deffunc Improper() = { [k,1]: not contradiction };
::>                                                      *129
::> 129: Invalid free variables in a Fraenkel operator

The error above is that, although k is Nat iff k is Element of NAT, the Fraenkel constructor requires its variables to widen to some 'Element of'. The fix is to change the type of k:

    reserve k for Element of NAT;

-- GregFrascadore - 2009-05-24