==========================================
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 '$applySubstitution['Q:Qid, 'S:Substitution] = 'Q:Qid [
    owise] .
eq '$applySubstitution['V:Variable, '_;_['S:Substitution, '_<-_['V:Variable,
    'T:Term]]] = 'T:Term [none] .
eq '$applySubstitution['_`,_['T:Term, 'TL:NeTermList], 'S:Substitution] =
    '_`,_['$applySubstitution['T:Term, 'S:Substitution], '$applySubstitution[
    'TL:NeTermList, 'S:Substitution]] [none] .
eq '$applySubstitution['_`[_`]['Q:Qid, 'TL:NeTermList], 'S:Substitution] =
    '_`[_`]['Q:Qid, '$applySubstitution['TL:NeTermList, 'S:Substitution]] [
    none] .
eq '$card['none.EmptyQidSet, '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.EmptyQidSet, '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.EmptyQidSet, '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.EmptyQidSet] [none] .
eq '_\_['S:QidSet, 'none.EmptyQidSet] = 'S:QidSet [none] .
eq '__['A:Attr, 'A:Attr] = 'A:Attr [none] .
eq '__['D:StratDefinition, 'D:StratDefinition] = 'D:StratDefinition [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 '__['O:StratDecl, 'O:StratDecl] = 'O:StratDecl [none] .
eq '__['R:Rule, 'R:Rule] = 'R:Rule [none] .
eq '__['S:SortMapping, 'S:SortMapping] = 'S:SortMapping [none] .
eq '__['S:StratMapping, 'S:StratMapping] = 'S:StratMapping [none] .
eq '__['S:SubsortDecl, 'S:SubsortDecl] = 'S:SubsortDecl [none] .
eq '_`,_['U:UsingPair, 'U:UsingPair] = 'U:UsingPair [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.EmptyQidSet, '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] = 'sth_is_sorts_._______endsth['Q:Qid, 'including_.['Q:Qid],
    'none.EmptyQidSet, 'none.SubsortDeclSet, 'none.OpDeclSet, 'none.MembAxSet,
    'none.EquationSet, 'none.RuleSet, 'none.StratDeclSet, 'none.StratDefSet] [
    none] .
eq 'append['A:NatList, 'L:NatList] = '__['A:NatList, 'L:NatList] [none] .
eq 'append['A:QidList, 'L:QidList] = '__['A:QidList, 'L:QidList] [none] .
eq 'applySubstitution['M:Module, 'T:Term, 'S:Substitution] = 'getTerm[
    'metaNormalize['M:Module, '$applySubstitution['T:Term, 'S:Substitution]]] [
    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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'EQS:EquationSet [
    none] .
eq 'getEqs['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = '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,
    'TMS:StratMappingSet]] = '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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList,
    'SS:SortSet, 'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet,
    'EQS:EquationSet, 'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] =
    'IL:ImportList [none] .
eq 'getImports['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList,
    'SS:SortSet, 'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet,
    'EQS:EquationSet, 'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] =
    '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 'getLhsSubstitution['`{_`,_`,_`}['LS:Substitution, 'RS:Substitution,
    'V:Qid]] = 'LS:Substitution [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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'MAS:MembAxSet [
    none] .
eq 'getMbs['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = '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 'getMoreVariantsInLayerFlag['`{_`,_`,_`,_`,_`}['T:Term, 'S:Substitution,
    'Q:Qid, 'P:Parent, 'B:Bool]] = 'B:Bool [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['smod_is_sorts_._______endsm['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'Q:Qid [none] .
eq 'getName['smod_is_sorts_._______endsm['_`{_`}['Q:Qid,
    'PDL:ParameterDeclList], 'IL:ImportList, 'SS:SortSet, 'SSDS:SubsortDeclSet,
    'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet, 'RLS:RuleSet,
    'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'Q:Qid [none] .
eq 'getName['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = '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,
    'TMS:StratMappingSet]] = 'Q:Qid [none] .
eq 'getName['view_from_to_is___endv['_`{_`}['Q:Qid, 'PDL:ParameterDeclList],
    'ME:ModuleExpression, 'ME':ModuleExpression, 'SMS:SortMappingSet,
    'OMS:OpMappingSet, 'TMS:StratMappingSet]] = 'Q:Qid [none] .
eq 'getOpMappings['view_from_to_is___endv['Q:Qid, 'ME:ModuleExpression,
    'ME':ModuleExpression, 'SMS:SortMappingSet, 'OMS:OpMappingSet,
    'TMS:StratMappingSet]] = '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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'OPDS:OpDeclSet [
    none] .
eq 'getOps['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = '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 'getParent['`{_`,_`,_`,_`,_`}['T:Term, 'S:Substitution, 'Q:Qid, 'P:Parent,
    'B:Bool]] = 'P:Parent [none] .
eq 'getRhsSubstitution['`{_`,_`,_`}['LS:Substitution, 'RS:Substitution,
    'V:Qid]] = 'RS:Substitution [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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'RLS:RuleSet [
    none] .
eq 'getRls['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = '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 'getRule['`{_`,_`,_`}['T:Term, 'T:Type, 'R:Rule]] = 'R:Rule [none] .
eq 'getRuleSubstitution['`{_`,_`,_`,_`,_`,_`,_`}['T:Term, 'T:Type, 'C:Context,
    'L:Qid, 'TS:Substitution, 'RS:Substitution, 'V:Qid]] = 'RS:Substitution [
    none] .
eq 'getSds['fmod_is_sorts_.____endfm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet]] =
    'none.StratDefSet [none] .
eq 'getSds['fth_is_sorts_.____endfth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet]] =
    'none.StratDefSet [none] .
eq 'getSds['mod_is_sorts_._____endm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet]] = 'none.StratDefSet [none] .
eq 'getSds['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'STDFS:StratDefSet
    [none] .
eq 'getSds['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'STDFS:StratDefSet
    [none] .
eq 'getSds['th_is_sorts_._____endth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet]] = 'none.StratDefSet [none] .
eq 'getSortMappings['view_from_to_is___endv['Q:Qid, 'ME:ModuleExpression,
    'ME':ModuleExpression, 'SMS:SortMappingSet, 'OMS:OpMappingSet,
    'TMS:StratMappingSet]] = '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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList,
    'SS:SortSet, 'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet,
    'EQS:EquationSet, 'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] =
    'SS:SortSet [none] .
eq 'getSorts['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = '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 'getStratMappings['view_from_to_is___endv['Q:Qid, 'ME:ModuleExpression,
    'ME':ModuleExpression, 'SMS:SortMappingSet, 'OMS:OpMappingSet,
    'TMS:StratMappingSet]] = 'TMS:StratMappingSet [none] .
eq 'getStrats['fmod_is_sorts_.____endfm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet]] =
    'none.StratDeclSet [none] .
eq 'getStrats['fth_is_sorts_.____endfth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet]] =
    'none.StratDeclSet [none] .
eq 'getStrats['mod_is_sorts_._____endm['H:Header, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet]] = 'none.StratDeclSet [none] .
eq 'getStrats['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList,
    'SS:SortSet, 'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet,
    'EQS:EquationSet, 'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] =
    'STDS:StratDeclSet [none] .
eq 'getStrats['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] = 'STDS:StratDeclSet
    [none] .
eq 'getStrats['th_is_sorts_._____endth['Q:Qid, 'IL:ImportList, 'SS:SortSet,
    'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet, 'EQS:EquationSet,
    'RLS:RuleSet]] = 'none.StratDeclSet [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['smod_is_sorts_._______endsm['H:Header, 'IL:ImportList,
    'SS:SortSet, 'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet,
    'EQS:EquationSet, 'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] =
    'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['sth_is_sorts_._______endsth['Q:Qid, 'IL:ImportList,
    'SS:SortSet, 'SSDS:SubsortDeclSet, 'OPDS:OpDeclSet, 'MAS:MembAxSet,
    'EQS:EquationSet, 'RLS:RuleSet, 'STDS:StratDeclSet, 'STDFS:StratDefSet]] =
    '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, 'S:Substitution, 'Q:Qid,
    'P:Parent, 'B:Bool]] = 'S:Substitution [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 'getSubstitution['`{_`,_`}['S:Substitution, 'V:Qid]] = '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, 'S:Substitution, 'Q:Qid, 'P:Parent,
    'B:Bool]] = 'T:Term [none] .
eq 'getTerm['`{_`,_`,_`,_`}['T:Term, 'T:Type, 'S:Substitution, 'C:Context]] =
    'T:Term [none] .
eq 'getTerm['`{_`,_`,_`}['T:Term, 'T:Type, 'R:Rule]] = '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,
    'TMS:StratMappingSet]] = '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, 'R:Rule]] = '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 'getVariableFamily['`{_`,_`,_`,_`,_`}['T:Term, 'S:Substitution, 'Q:Qid,
    'P:Parent, 'B:Bool]] = 'Q:Qid [none] .
eq 'getVariableFamily['`{_`,_`,_`}['LS:Substitution, 'RS:Substitution, 'V:Qid]]
    = 'V:Qid [none] .
eq 'getVariableFamily['`{_`,_`}['S: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.EmptyQidSet] [none] .
eq 'intersection['S:QidSet, 'none.EmptyQidSet] = 'none.EmptyQidSet [none] .
eq 'last['__['L:NatList, 'E:Nat]] = 'E:Nat [none] .
eq 'last['__['L:QidList, 'E:Qid]] = 'E:Qid [none] .
eq 'metaNarrowingApply['M:Module, 'T:Term, 'TL:TermList, 'Q:Qid, 'N:Nat] =
    'metaNarrowingApply['M:Module, 'T:Term, 'TL:TermList, 'Q:Qid,
    'none.VariantOptionSet, 'N:Nat] [none] .
eq 'metaNarrowingSearch['M:Module, 'T:Term, 'T2:Term, 'S:Qid, 'B:Bound, 'F:Qid,
    'N:Nat] = 'metaNarrowingSearch['M:Module, 'T:Term, 'T2:Term, 'S:Qid,
    'B:Bound, 'F:Qid, 'none.VariantOptionSet, 'N:Nat] [none] .
eq 'metaNarrowingSearchPath['M:Module, 'T:Term, 'T2:Term, 'S:Qid, 'B:Bound,
    'F:Qid, 'N:Nat] = 'metaNarrowingSearchPath['M:Module, 'T:Term, 'T2:Term,
    'S:Qid, 'B:Bound, 'F:Qid, 'none.VariantOptionSet, 'N:Nat] [none] .
eq 'metaParse['M:Module, 'Q:QidList, 'T:Type?] = 'metaParse['M:Module,
    'none.EmptyQidSet, 'Q:QidList, 'T:Type?] [none] .
eq 'metaPrettyPrint['M:Module, 'T:Term] = 'metaPrettyPrint['M:Module,
    'none.EmptyQidSet, 'T:Term, '__['mixfix.PrintOption, '__['flat.PrintOption,
    '__['format.PrintOption, '__['number.PrintOption, 'rat.PrintOption]]]],
    'none.EmptyQidSet] [none] .
eq 'metaPrettyPrint['M:Module, 'T:Term, 'P:PrintOptionSet] = 'metaPrettyPrint[
    'M:Module, 'none.EmptyQidSet, 'T:Term, 'P:PrintOptionSet,
    'none.EmptyQidSet] [none] .
eq 'metaPrettyPrint['M:Module, 'VS:VariableSet, 'T:Term, 'P:PrintOptionSet] =
    'metaPrettyPrint['M:Module, 'VS:VariableSet, 'T:Term, 'P:PrintOptionSet,
    'none.EmptyQidSet] [none] .
eq 'metaVariantDisjointUnify['M:Module, 'U:UnificationProblem, 'TL:TermList,
    'Q:Qid, 'N:Nat] = 'metaVariantDisjointUnify['M:Module,
    'U:UnificationProblem, 'TL:TermList, 'Q:Qid, 'none.VariantOptionSet,
    'N:Nat] [none] .
eq 'metaVariantUnify['M:Module, 'U:UnificationProblem, 'TL:TermList, 'Q:Qid,
    'N:Nat] = 'metaVariantUnify['M:Module, 'U:UnificationProblem, 'TL:TermList,
    'Q:Qid, 'none.VariantOptionSet, 'N:Nat] [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.