==========================================
reduce in META-LEVEL : upEqs('ATTR-TEST, true) .
rewrites: 1
result EquationSet: eq '_and_['A:Bool,'A:Bool] = 'A:Bool [none] .
eq '_and_['A:Bool,'_xor_['B:Bool,'C:Bool]] = '_xor_['_and_['A:Bool,'B:Bool],
    '_and_['A:Bool,'C:Bool]] [none] .
eq '_and_['false.Bool,'A:Bool] = 'false.Bool [none] .
eq '_and_['true.Bool,'A:Bool] = 'A:Bool [none] .
eq '_implies_['A:Bool,'B:Bool] = 'not_['_xor_['A:Bool,'_and_['A:Bool,'B:Bool]]]
    [none] .
eq '_or_['A:Bool,'B:Bool] = '_xor_['_and_['A:Bool,'B:Bool],'_xor_['A:Bool,
    'B:Bool]] [none] .
eq '_xor_['A:Bool,'A:Bool] = 'false.Bool [none] .
eq '_xor_['false.Bool,'A:Bool] = 'A:Bool [none] .
eq 'f['X:Foo,'a.Foo] = 'X:Foo [label('first) metadata(
    "this is the first equation")] .
eq 'f['b.Foo,'Y:Foo] = 'b.Foo [metadata("this is the second equation")] .
eq 'not_['A:Bool] = '_xor_['true.Bool,'A:Bool] [none] .
==========================================
reduce in META-LEVEL : upRls('ATTR-TEST, true) .
rewrites: 1
result Rule: rl 'a.Foo => 'b.Foo [label('r1)] .
==========================================
reduce in META-LEVEL : upMbs('ATTR-TEST, true) .
rewrites: 1
result MembAx: mb 'a.Foo : 'Foo [label('baz) metadata("this is an mb")] .
==========================================
reduce in META-LEVEL : upEqs('ATTR-TEST, false) .
rewrites: 1
result EquationSet: eq 'f['X:Foo,'a.Foo] = 'X:Foo [label('first) metadata(
    "this is the first equation")] .
eq 'f['b.Foo,'Y:Foo] = 'b.Foo [metadata("this is the second equation")] .
==========================================
reduce in META-LEVEL : upRls('ATTR-TEST, false) .
rewrites: 1
result Rule: rl 'a.Foo => 'b.Foo [label('r1)] .
==========================================
reduce in META-LEVEL : upMbs('ATTR-TEST, false) .
rewrites: 1
result MembAx: mb 'a.Foo : 'Foo [label('baz) metadata("this is an mb")] .
==========================================
reduce in META-LEVEL : upRls('BOOL, true) .
rewrites: 1
result RuleSet: (none).RuleSet
==========================================
reduce in META-LEVEL : upRls('KNIGHT, true) .
rewrites: 1
result RuleSet: rl 'knight['0.Zero] => '`[_`,_`]['s_['0.Zero],'s_['0.Zero]] [
    none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_['0.Zero]],
    '_+_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_['0.Zero]],
    '_-_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_^2['0.Zero]],
    '_+_['Y:Int,'s_['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_^2['0.Zero]],
    '_-_['Y:Int,'s_['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_['0.Zero]],
    '_+_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_['0.Zero]],
    '_-_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_^2['0.Zero]],
    '_+_['Y:Int,'s_['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_^2['0.Zero]],
    '_-_['Y:Int,'s_['0.Zero]]] [none] .
crl 'knight['N:Int] => '__['L:List,'__['P:Pair,'Q:Pair]] if '_>_['N:Int,
    '0.Zero] = 'true.Bool /\ 'knight['_-_['N:Int,'s_['0.Zero]]] => '__['L:List,
    'P:Pair] /\ 'move_['P:Pair] => 'Q:Pair /\ 'legal['Q:Pair] = 'true.Bool /\
    'not_['contains['__['L:List,'P:Pair],'Q:Pair]] = 'true.Bool [none] .
==========================================
rewrite in INTROSPECTION : rules .
rewrites: 2
result Rule: rl 'rules.RuleSet => 'upRls[''INTROSPECTION.Sort,'false.Bool] [
    none] .
==========================================
rewrite in SELF-REFLECTION : myRules .
rewrites: 2
result RuleSet: rl 'allRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,
    'true.Bool] [none] .
rl 'myRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,'false.Bool] [none] .
==========================================
rewrite in SELF-REFLECTION : allRules .
rewrites: 2
result RuleSet: rl 'allRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,
    'true.Bool] [none] .
rl 'myRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,'false.Bool] [none] .
rl 'rules.RuleSet => 'upRls[''INTROSPECTION.Sort,'false.Bool] [none] .
==========================================
reduce in META-LEVEL : upEqs('META-LEVEL, true) .
rewrites: 1
result EquationSet: eq '$card['none.EmptyTypeSet,'C:Nat] = 'C:Nat [none] .
eq '$card['_;_['E:Qid,'S:QidSet],'C:Nat] = '$card['S:QidSet,'_+_['C:Nat,'s_[
    '0.Zero]]] [owise] .
eq '$card['_;_['N:NeQidSet,'N:NeQidSet,'S:QidSet],'C:Nat] = '$card['_;_[
    'N:NeQidSet,'S:QidSet],'C:Nat] [none] .
eq '$diff['none.EmptyTypeSet,'S':QidSet,'A:QidSet] = 'A:QidSet [none] .
eq '$diff['_;_['E:Qid,'S:QidSet],'S':QidSet,'A:QidSet] = '$diff['S:QidSet,
    'S':QidSet,'if_then_else_fi['_in_['E:Qid,'S':QidSet],'A:QidSet,'_;_['E:Qid,
    'A:QidSet]]] [none] .
eq '$intersect['none.EmptyTypeSet,'S':QidSet,'A:QidSet] = 'A:QidSet [none] .
eq '$intersect['_;_['E:Qid,'S:QidSet],'S':QidSet,'A:QidSet] = '$intersect[
    'S:QidSet,'S':QidSet,'if_then_else_fi['_in_['E:Qid,'S':QidSet],'_;_['E:Qid,
    'A:QidSet],'A:QidSet]] [none] .
eq '$reverse['nil.NatList,'A:NatList] = 'A:NatList [none] .
eq '$reverse['nil.TypeList,'A:QidList] = 'A:QidList [none] .
eq '$reverse['__['E:Nat,'L:NatList],'A:NatList] = '$reverse['L:NatList,'__[
    'E:Nat,'A:NatList]] [none] .
eq '$reverse['__['E:Qid,'L:QidList],'A:QidList] = '$reverse['L:QidList,'__[
    'E:Qid,'A:QidList]] [none] .
eq '$size['nil.NatList,'C:Nat] = 'C:Nat [none] .
eq '$size['nil.TypeList,'C:Nat] = 'C:Nat [none] .
eq '$size['__['E:Nat,'L:NatList],'C:Nat] = '$size['L:NatList,'_+_['C:Nat,'s_[
    '0.Zero]]] [none] .
eq '$size['__['E:Qid,'L:QidList],'C:Nat] = '$size['L:QidList,'_+_['C:Nat,'s_[
    '0.Zero]]] [none] .
eq '_;_['A:Assignment,'A:Assignment] = 'A:Assignment [none] .
eq '_;_['N:NeQidSet,'N:NeQidSet] = 'N:NeQidSet [none] .
eq '_;_['T:TypeList,'T:TypeList] = 'T:TypeList [none] .
eq '_\_['S:QidSet,'N:NeQidSet] = '$diff['S:QidSet,'N:NeQidSet,
    'none.EmptyTypeSet] [none] .
eq '_\_['S:QidSet,'none.EmptyTypeSet] = 'S:QidSet [none] .
eq '__['A:Attr,'A:Attr] = 'A:Attr [none] .
eq '__['E:Equation,'E:Equation] = 'E:Equation [none] .
eq '__['M:MembAx,'M:MembAx] = 'M:MembAx [none] .
eq '__['O:OpDecl,'O:OpDecl] = 'O:OpDecl [none] .
eq '__['O:OpMapping,'O:OpMapping] = 'O:OpMapping [none] .
eq '__['R:Rule,'R:Rule] = 'R:Rule [none] .
eq '__['S:SortMapping,'S:SortMapping] = 'S:SortMapping [none] .
eq '__['S:SubsortDecl,'S:SubsortDecl] = 'S:SubsortDecl [none] .
eq '_and-then_['false.Bool,'B:`[Bool`]] = 'false.Bool [none] .
eq '_and-then_['true.Bool,'B:`[Bool`]] = 'B:`[Bool`] [none] .
eq '_and_['A:Bool,'A:Bool] = 'A:Bool [none] .
eq '_and_['A:Bool,'_xor_['B:Bool,'C:Bool]] = '_xor_['_and_['A:Bool,'B:Bool],
    '_and_['A:Bool,'C:Bool]] [none] .
eq '_and_['false.Bool,'A:Bool] = 'false.Bool [none] .
eq '_and_['true.Bool,'A:Bool] = 'A:Bool [none] .
eq '_implies_['A:Bool,'B:Bool] = 'not_['_xor_['A:Bool,'_and_['A:Bool,'B:Bool]]]
    [none] .
eq '_in_['E:Qid,'S:QidSet] = 'false.Bool [owise] .
eq '_in_['E:Qid,'_;_['E:Qid,'S:QidSet]] = 'true.Bool [none] .
eq '_or-else_['false.Bool,'B:`[Bool`]] = 'B:`[Bool`] [none] .
eq '_or-else_['true.Bool,'B:`[Bool`]] = 'true.Bool [none] .
eq '_or_['A:Bool,'B:Bool] = '_xor_['_and_['A:Bool,'B:Bool],'_xor_['A:Bool,
    'B:Bool]] [none] .
eq '_psubset_['S:QidSet,'S':QidSet] = '_and-then_['_=/=_['S:QidSet,'S':QidSet],
    '_subset_['S:QidSet,'S':QidSet]] [none] .
eq '_subset_['none.EmptyTypeSet,'S':QidSet] = 'true.Bool [none] .
eq '_subset_['_;_['E:Qid,'S:QidSet],'S':QidSet] = '_and-then_['_in_['E:Qid,
    'S':QidSet],'_subset_['S:QidSet,'S':QidSet]] [none] .
eq '_xor_['A:Bool,'A:Bool] = 'false.Bool [none] .
eq '_xor_['false.Bool,'A:Bool] = 'A:Bool [none] .
eq '`[_`]['Q:Qid] = 'th_is_sorts_._____endth['Q:Qid,'including_.['Q:Qid],
    'none.EmptyTypeSet,'none.SubsortDeclSet,'none.OpDeclSet,'none.MembAxSet,
    'none.EquationSet,'none.RuleSet] [none] .
eq 'append['A:NatList,'L:NatList] = '__['A:NatList,'L:NatList] [none] .
eq 'append['A:QidList,'L:QidList] = '__['A:QidList,'L:QidList] [none] .
eq 'delete['E:Qid,'S:QidSet] = 'S:QidSet [owise] .
eq 'delete['E:Qid,'_;_['E:Qid,'S:QidSet]] = 'delete['E:Qid,'S:QidSet] [none] .
eq 'front['__['L:NatList,'E:Nat]] = 'L:NatList [none] .
eq 'front['__['L:QidList,'E:Qid]] = 'L:QidList [none] .
eq 'getAccumulatedSubstitution['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,
    'U:Substitution,'UV:Qid,'T:Term,'T:Type,'A:Substitution]] = 'A:Substitution
    [none] .
eq 'getAccumulatedSubstitution['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,
    'A:Substitution,'SV:Qid,'U:Substitution,'UV:Qid]] = 'A:Substitution [none]
    .
eq 'getContext['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,'U:Substitution,
    'UV:Qid,'T:Term,'T:Type,'A:Substitution]] = 'C:Context [none] .
eq 'getContext['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,'L:Qid,
    'TS:Substitution,'RS:Substitution,'V:Qid]] = 'C:Context [none] .
eq 'getContext['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,'C:Context]] =
    'C:Context [none] .
eq 'getContext['`{_`,_`}['S:Substitution,'C:Context]] = 'C:Context [none] .
eq 'getEqs['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'EQS:EquationSet [none] .
eq 'getEqs['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'EQS:EquationSet [none] .
eq 'getEqs['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'EQS:EquationSet [none] .
eq 'getEqs['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'EQS:EquationSet [none] .
eq 'getFrom['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
    'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
    'ME:ModuleExpression [none] .
eq 'getImports['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'IL:ImportList [none] .
eq 'getImports['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'IL:ImportList [none] .
eq 'getImports['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'IL:ImportList [none] .
eq 'getImports['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'IL:ImportList [none] .
eq 'getInitialSubstitution['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,
    'S:Substitution,'T:NarrowingTrace,'U:Substitution,'UV:Qid]] =
    'S:Substitution [none] .
eq 'getInitialTerm['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,
    'T:NarrowingTrace,'U:Substitution,'UV:Qid]] = 'T:Term [none] .
eq 'getInitialType['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,
    'T:NarrowingTrace,'U:Substitution,'UV:Qid]] = 'T:Type [none] .
eq 'getLabel['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,'U:Substitution,
    'UV:Qid,'T:Term,'T:Type,'A:Substitution]] = 'L:Qid [none] .
eq 'getLabel['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,'L:Qid,
    'TS:Substitution,'RS:Substitution,'V:Qid]] = 'L:Qid [none] .
eq 'getMbs['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'MAS:MembAxSet [none] .
eq 'getMbs['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'MAS:MembAxSet [none] .
eq 'getMbs['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'MAS:MembAxSet [none] .
eq 'getMbs['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'MAS:MembAxSet [none] .
eq 'getName['C:Constant] = 'qid['substr['string['C:Constant],'0.Zero,'rfind[
    'string['C:Constant],'".".Char,'length['string['C:Constant]]]]] [none] .
eq 'getName['V:Variable] = 'qid['substr['string['V:Variable],'0.Zero,'rfind[
    'string['V:Variable],'":".Char,'length['string['V:Variable]]]]] [none] .
eq 'getName['fmod_is_sorts_.____endfm['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'Q:Qid [none] .
eq 'getName['fmod_is_sorts_.____endfm['_`{_`}['Q:Qid,'PDL:ParameterDeclList],
    'IL:ImportList,'SS:SortSet,'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,
    'MAS:MembAxSet,'EQS:EquationSet]] = 'Q:Qid [none] .
eq 'getName['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'Q:Qid [none] .
eq 'getName['mod_is_sorts_._____endm['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'Q:Qid [none] .
eq 'getName['mod_is_sorts_._____endm['_`{_`}['Q:Qid,'PDL:ParameterDeclList],
    'IL:ImportList,'SS:SortSet,'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,
    'MAS:MembAxSet,'EQS:EquationSet,'RLS:RuleSet]] = 'Q:Qid [none] .
eq 'getName['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'Q:Qid [none] .
eq 'getName['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
    'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] = 'Q:Qid [
    none] .
eq 'getOpMappings['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
    'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
    'OMS:OpMappingSet [none] .
eq 'getOps['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'OPDS:OpDeclSet [none] .
eq 'getOps['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'OPDS:OpDeclSet [none] .
eq 'getOps['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'OPDS:OpDeclSet [none] .
eq 'getOps['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'OPDS:OpDeclSet [none] .
eq 'getRls['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'none.RuleSet [none] .
eq 'getRls['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'none.RuleSet [none] .
eq 'getRls['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'RLS:RuleSet [none] .
eq 'getRls['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'RLS:RuleSet [none] .
eq 'getRuleSubstitution['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,
    'L:Qid,'TS:Substitution,'RS:Substitution,'V:Qid]] = 'RS:Substitution [none]
    .
eq 'getSortMappings['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
    'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
    'SMS:SortMappingSet [none] .
eq 'getSorts['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'SS:SortSet [none] .
eq 'getSorts['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'SS:SortSet [none] .
eq 'getSorts['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'SS:SortSet [none] .
eq 'getSorts['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'SS:SortSet [none] .
eq 'getStateVariableFamily['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,
    'A:Substitution,'SV:Qid,'U:Substitution,'UV:Qid]] = 'SV:Qid [none] .
eq 'getSubsorts['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
    'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
    'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
    'RLS:RuleSet]] = 'SSDS:SubsortDeclSet [none] .
eq 'getSubstitution['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,
    'C:Context]] = 'S:Substitution [none] .
eq 'getSubstitution['`{_`,_`,_`}['T:Term,'T:Type,'S:Substitution]] =
    'S:Substitution [none] .
eq 'getSubstitution['`{_`,_`}['S:Substitution,'C:Context]] = 'S:Substitution [
    none] .
eq 'getTerm['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,'U:Substitution,'UV:Qid,
    'T:Term,'T:Type,'A:Substitution]] = 'T:Term [none] .
eq 'getTerm['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,'L:Qid,
    'TS:Substitution,'RS:Substitution,'V:Qid]] = 'T:Term [none] .
eq 'getTerm['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'A:Substitution,'SV:Qid,
    'U:Substitution,'UV:Qid]] = 'T:Term [none] .
eq 'getTerm['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,'C:Context]] =
    'T:Term [none] .
eq 'getTerm['`{_`,_`,_`}['T:Term,'T:Type,'S:Substitution]] = 'T:Term [none] .
eq 'getTerm['`{_`,_`}['T:Term,'T:Type]] = 'T:Term [none] .
eq 'getTermSubstitution['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,
    'L:Qid,'TS:Substitution,'RS:Substitution,'V:Qid]] = 'TS:Substitution [none]
    .
eq 'getTo['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
    'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
    'ME':ModuleExpression [none] .
eq 'getTrace['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,
    'T:NarrowingTrace,'U:Substitution,'UV:Qid]] = 'T:NarrowingTrace [none] .
eq 'getType['C:Constant] = 'qid['substr['string['C:Constant],'_+_['s_['0.Zero],
    'rfind['string['C:Constant],'".".Char,'length['string['C:Constant]]]],
    'length['string['C:Constant]]]] [none] .
eq 'getType['V:Variable] = 'qid['substr['string['V:Variable],'_+_['s_['0.Zero],
    'rfind['string['V:Variable],'":".Char,'length['string['V:Variable]]]],
    'length['string['V:Variable]]]] [none] .
eq 'getType['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,'U:Substitution,'UV:Qid,
    'T:Term,'T:Type,'A:Substitution]] = 'T:Type [none] .
eq 'getType['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,'L:Qid,
    'TS:Substitution,'RS:Substitution,'V:Qid]] = 'T:Type [none] .
eq 'getType['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'A:Substitution,'SV:Qid,
    'U:Substitution,'UV:Qid]] = 'T:Type [none] .
eq 'getType['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,'C:Context]] =
    'T:Type [none] .
eq 'getType['`{_`,_`,_`}['T:Term,'T:Type,'S:Substitution]] = 'T:Type [none] .
eq 'getType['`{_`,_`}['T:Term,'T:Type]] = 'T:Type [none] .
eq 'getUnifier['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,'U:Substitution,
    'UV:Qid,'T:Term,'T:Type,'A:Substitution]] = 'U:Substitution [none] .
eq 'getUnifier['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'A:Substitution,'SV:Qid,
    'U:Substitution,'UV:Qid]] = 'U:Substitution [none] .
eq 'getUnifier['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,
    'T:NarrowingTrace,'U:Substitution,'UV:Qid]] = 'U:Substitution [none] .
eq 'getUnifierVariableFamily['`{_`,_`,_`,_`,_`,_`,_`}['C:Context,'L:Qid,
    'U:Substitution,'UV:Qid,'T:Term,'T:Type,'A:Substitution]] = 'UV:Qid [none]
    .
eq 'getUnifierVariableFamily['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,
    'A:Substitution,'SV:Qid,'U:Substitution,'UV:Qid]] = 'UV:Qid [none] .
eq 'getUnifierVariableFamily['`{_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,
    'S:Substitution,'T:NarrowingTrace,'U:Substitution,'UV:Qid]] = 'UV:Qid [
    none] .
eq 'getVariableFamily['`{_`,_`,_`,_`,_`,_`,_`}['T:Term,'T:Type,'C:Context,
    'L:Qid,'TS:Substitution,'RS:Substitution,'V:Qid]] = 'V:Qid [none] .
eq 'head['__['E:Nat,'L:NatList]] = 'E:Nat [none] .
eq 'head['__['E:Qid,'L:QidList]] = 'E:Qid [none] .
eq 'insert['E:Qid,'S:QidSet] = '_;_['E:Qid,'S:QidSet] [none] .
eq 'intersection['S:QidSet,'N:NeQidSet] = '$intersect['S:QidSet,'N:NeQidSet,
    'none.EmptyTypeSet] [none] .
eq 'intersection['S:QidSet,'none.EmptyTypeSet] = 'none.EmptyTypeSet [none] .
eq 'last['__['L:NatList,'E:Nat]] = 'E:Nat [none] .
eq 'last['__['L:QidList,'E:Qid]] = 'E:Qid [none] .
eq 'metaPrettyPrint['M:Module,'T:Term] = 'metaPrettyPrint['M:Module,'T:Term,
    '__['mixfix.PrintOption,'__['flat.PrintOption,'__['format.PrintOption,'__[
    'number.PrintOption,'rat.PrintOption]]]]] [none] .
eq 'not_['A:Bool] = '_xor_['true.Bool,'A:Bool] [none] .
eq 'occurs['E:Nat,'nil.NatList] = 'false.Bool [none] .
eq 'occurs['E:Nat,'__['E':Nat,'L:NatList]] = 'if_then_else_fi['_==_['E:Nat,
    'E':Nat],'true.Bool,'occurs['E:Nat,'L:NatList]] [none] .
eq 'occurs['E:Qid,'nil.TypeList] = 'false.Bool [none] .
eq 'occurs['E:Qid,'__['E':Qid,'L:QidList]] = 'if_then_else_fi['_==_['E:Qid,
    'E':Qid],'true.Bool,'occurs['E:Qid,'L:QidList]] [none] .
eq 'reverse['L:NatList] = '$reverse['L:NatList,'nil.NatList] [none] .
eq 'reverse['L:QidList] = '$reverse['L:QidList,'nil.TypeList] [none] .
eq 'size['L:NatList] = '$size['L:NatList,'0.Zero] [none] .
eq 'size['L:QidList] = '$size['L:QidList,'0.Zero] [none] .
eq 'tail['__['E:Nat,'L:NatList]] = 'L:NatList [none] .
eq 'tail['__['E:Qid,'L:QidList]] = 'L:QidList [none] .
eq 'union['S:QidSet,'S':QidSet] = '_;_['S:QidSet,'S':QidSet] [none] .
eq '|_|['S:QidSet] = '$card['S:QidSet,'0.Zero] [none] .
Bye.