mod CTXT is
        including RUNTIME-PRELUDE .
        op $@& : Trm Trm -> Trm [ assoc ] .
        op $SEQ : Trm Trm -> Trm [ comm ] .
        op $nat-mult : Trm Trm -> Trm [ assoc comm ] .
        op $nat-plus : Trm Trm -> Trm [ assoc comm ] .
        op $union : Trm Trm -> Trm [ assoc comm ] .
        mb      ( ( ( 'ST { 0 } ) ( 'Prop { 0 } ) ) ( 'Type { 0 } ) ) : TrueTrm .
        mb      ( ( ( 'nat_eq { 0 } ) ( '0 { 0 } ) ) ( '0 { 0 } ) ) : TrueTrm .
        mb      ( ( ( 'nat_le { 0 } ) ( '0 { 0 } ) ) @i:Trm ) : TrueTrm .
        mb      ( ( 'Not { 0 } ) ( ( ( 'nat_eq { 0 } ) ( ( 'suc { 0 } ) @i:Trm ) ) ( '0 { 0 } ) ) ) : TrueTrm .
        mb      ( ( 'Not { 0 } ) ( ( ( 'nat_eq { 0 } ) ( '0 { 0 } ) ) ( ( 'suc { 0 } ) @i:Trm ) ) ) : TrueTrm .
        mb      ( 'True { 0 } ) : TrueTrm .
        cmb     $SEQ ( @x:Trm , @y:Trm ) : TrueTrm
                if      ( ( ( 'EQ { 0 } ) @x:Trm ) @y:Trm ) : TrueTrm .
        cmb     ( ( ( 'And { 0 } ) @A:Trm ) @B:Trm ) : TrueTrm
                if      @A:Trm : TrueTrm /\
                        @B:Trm : TrueTrm .
        cmb     ( ( ( 'Or { 0 } ) @A:Trm ) @B:Trm ) : TrueTrm
                if      @A:Trm : TrueTrm .
        cmb     ( ( ( 'Or { 0 } ) @A:Trm ) @B:Trm ) : TrueTrm
                if      @B:Trm : TrueTrm .
        cmb     ( ( ( 'nat_eq { 0 } ) ( ( 'suc { 0 } ) @i:Trm ) ) ( ( 'suc { 0 } ) @j:Trm ) ) : TrueTrm
                if      ( ( ( 'nat_eq { 0 } ) @i:Trm ) @j:Trm ) : TrueTrm .
        cmb     ( ( ( 'nat_le { 0 } ) ( ( 'suc { 0 } ) @i:Trm ) ) ( ( 'suc { 0 } ) @j:Trm ) ) : TrueTrm
                if      ( ( ( 'nat_le { 0 } ) @i:Trm ) @j:Trm ) : TrueTrm .
        cmb     ( ( ( 'nat_lt { 0 } ) @i:Trm ) @j:Trm ) : TrueTrm
                if      ( ( 'Not { 0 } ) ( ( ( 'nat_eq { 0 } ) @i:Trm ) @j:Trm ) ) : TrueTrm /\
                        ( ( ( 'nat_le { 0 } ) @i:Trm ) @j:Trm ) : TrueTrm .
        cmb     ( ( 'Not { 0 } ) ( ( ( 'nat_eq { 0 } ) ( ( 'suc { 0 } ) @i:Trm ) ) ( ( 'suc { 0 } ) @j:Trm ) ) ) : TrueTrm
                if      ( ( 'Not { 0 } ) ( ( ( 'nat_eq { 0 } ) @i:Trm ) @j:Trm ) ) : TrueTrm .
        cmb     ( ( 'Not { 0 } ) ( ( ( 'nat_le { 0 } ) @i:Trm ) @j:Trm ) ) : TrueTrm
                if      ( ( ( 'nat_lt { 0 } ) @j:Trm ) @i:Trm ) : TrueTrm .
        eq      $nat-mult ( @i:Trm , ( ( 'suc { 0 } ) @j:Trm ) ) =
                $nat-plus ( @i:Trm , $nat-mult ( @i:Trm , @j:Trm ) ) .
        eq      $nat-mult ( @i:Trm , ( ( 'suc { 0 } ) ( '0 { 0 } ) ) ) =
                @i:Trm .
        eq      $nat-mult ( ( '0 { 0 } ) , @i:Trm ) =
                ( '0 { 0 } ) .
        eq      $nat-plus ( @i:Trm , ( ( 'suc { 0 } ) @j:Trm ) ) =
                ( ( 'suc { 0 } ) $nat-plus ( @i:Trm , @j:Trm ) ) .
        eq      $nat-plus ( ( '0 { 0 } ) , @i:Trm ) =
                @i:Trm .
        eq      ( S:Subst * $@& ( @1:Trm , @2:Trm ) ) =
                ( ( ( S:Subst * ( # ( '@& ){0}) ) ( S:Subst * @1:Trm ) ) ( S:Subst * @2:Trm ) ) .
        eq      ( S:Subst * $SEQ ( @1:Trm , @2:Trm ) ) =
                ( ( ( S:Subst * ( # ( 'SEQ ){0}) ) ( S:Subst * @1:Trm ) ) ( S:Subst * @2:Trm ) ) .
        eq      ( S:Subst * $nat-mult ( @1:Trm , @2:Trm ) ) =
                ( ( ( S:Subst * ( # ( 'nat_mult ){0}) ) ( S:Subst * @1:Trm ) ) ( S:Subst * @2:Trm ) ) .
        eq      ( S:Subst * $nat-plus ( @1:Trm , @2:Trm ) ) =
                ( ( ( S:Subst * ( # ( 'nat_plus ){0}) ) ( S:Subst * @1:Trm ) ) ( S:Subst * @2:Trm ) ) .
        eq      ( S:Subst * $union ( @1:Trm , @2:Trm ) ) =
                ( ( ( S:Subst * ( # ( 'union ){0}) ) ( S:Subst * @1:Trm ) ) ( S:Subst * @2:Trm ) ) .
        eq      ( ( ( '@& { 0 } ) @1:Trm ) @2:Trm ) =
                $@& ( @1:Trm , @2:Trm ) .
        eq      ( ( ( 'SEQ { 0 } ) @1:Trm ) @2:Trm ) =
                $SEQ ( @1:Trm , @2:Trm ) .
        eq      ( ( ( 'nat_minus { 0 } ) @i:Trm ) ( '0 { 0 } ) ) =
                @i:Trm .
        eq      ( ( ( 'nat_minus { 0 } ) ( ( 'suc { 0 } ) @i:Trm ) ) ( ( 'suc { 0 } ) @j:Trm ) ) =
                ( ( ( 'nat_minus { 0 } ) @i:Trm ) @j:Trm ) .
        eq      ( ( ( 'nat_mult { 0 } ) @1:Trm ) @2:Trm ) =
                $nat-mult ( @1:Trm , @2:Trm ) .
        eq      ( ( ( 'nat_plus { 0 } ) @1:Trm ) @2:Trm ) =
                $nat-plus ( @1:Trm , @2:Trm ) .
        eq      ( ( ( 'union { 0 } ) @1:Trm ) @2:Trm ) =
                $union ( @1:Trm , @2:Trm ) .
        eq      ( ( 'nat_fact { 0 } ) ( ( 'suc { 0 } ) @n:Trm ) ) =
                $nat-plus ( ( ( 'nat_fact { 0 } ) @n:Trm ) , $nat-mult ( @n:Trm , ( ( 'nat_fact { 0 } ) @n:Trm ) ) ) .
        eq      ( ( 'nat_fact { 0 } ) ( '0 { 0 } ) ) =
                ( ( 'suc { 0 } ) ( '0 { 0 } ) ) .
        eq      ( 'config { 0 } ) =
                ( ( ( 'union { 0 } ) ( ( 'F { 0 } ) ( '0 { 0 } ) ) ) ( ( ( 'union { 0 } ) ( ( ( 'union { 0 } ) ( ( ( 'union
    { 0 } ) ( ( ( 'union { 0 } ) ( ( ( 'union { 0 } ) ( ( ( 'EL { 0 } ) ( '@KAS { 0 } ) ) ( '@AS { 0 } ) ) ) ( ( ( 'EL { 0
    } ) ( '@server { 0 } ) ) ( '@S { 0 } ) ) ) ) ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@client-tcs { 0 } ) ( '@C { 0 } )
    ) ) ) ( '@kC { 0 } ) ) ) ) ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) ( '@TS { 0 } )
    ) ) ) ) ( '@kTS { 0 } ) ) ) ) ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } ) ( '@S {
    0 } ) ) ) ) ) ( '@kS { 0 } ) ) ) ) ( ( ( 'union { 0 } ) ( ( ( '@START-ASE { 0 } ) ( '@C { 0 } ) ) ( '@TS { 0 } ) ) ) (
    ( ( 'union { 0 } ) ( ( '@START-TGE { 0 } ) ( '@C { 0 } ) ) ) ( ( '@START-CSE { 0 } ) ( '@C { 0 } ) ) ) ) ) ) .
        crl     $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0
    } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( (
    '@TGS-ts { 0 } ) @@T:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 } ) @@n1:Trm ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( (
    'T_serverASE_answer { 0 } ) @@K:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) )
    @@kC:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) ) ) @@kT:Trm )
    ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kT:Trm ) ) $@& ( ( ( '@shK-msg { 0
    } ) @@AKey:Trm ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) ) , ( ( (
    '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kC:Trm ) ) $@& ( $@& ( ( ( '@shK-msg { 0 } ) @@AKey:Trm ) , ( ( '@nonce-msg {
    0 } ) @@n1:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm
    ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm
    ) ) ) @@kC:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) ) )
    @@kT:Trm ) )
                if      @@AKey:Trm := ( ( ( 'FRESH { 0 } ) ( ( ( '@shK { 0 } ) @@C:Trm ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) )
    @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( $union ( $union ( ( ( '@START-TGE { 0 } ) @@C:Trm ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( (
    ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm ) ) , ( ( ( 'T_clientTGE_req { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( ( ( ( (
    '@Auth { 0 } ) @@C:Trm ) @@X:Trm ) @@T:Trm ) @@AKey:Trm ) ) =>
                $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( @@X:Trm , ( ( ( '@encrypt { 0 }
    ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm
    ) ) ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) , ( ( '@princ-msg
    { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 }
    ) @@n2:Trm ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm ) ) , ( ( ( ( (
    '@Auth { 0 } ) @@C:Trm ) @@X:Trm ) @@T:Trm ) @@AKey:Trm ) ) , ( ( ( ( @@L:Trm @@C:Trm ) @@S:Trm ) @@T:Trm ) @@n2:Trm )
    )
                if      @@n2:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key {
    0 } ) @@kT:Trm ) ) $@& ( ( ( '@shK-msg { 0 } ) @@AKey:Trm ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) ( ( '@princ-msg {
    0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0
    } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( (
    '@server-ts { 0 } ) @@S:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 } ) @@n2:Trm ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( (
    'T_serverTGE_answer { 0 } ) @@T:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0
    } ) @@S:Trm ) ) ) ) @@kS:Trm ) ) =>
                $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kS:Trm ) ) $@& ( ( ( '@shK-msg { 0
    } ) @@SKey:Trm ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) ) , ( ( (
    '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) $@& ( $@& ( ( ( '@shK-msg { 0 } ) @@SKey:Trm ) , ( ( '@nonce-msg
    { 0 } ) @@n2:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } )
    @@S:Trm ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( (
    '@server-ts { 0 } ) @@S:Trm ) ) ) ) @@kS:Trm ) )
                if      @@SKey:Trm := ( ( ( 'FRESH { 0 } ) ( ( ( '@shK { 0 } ) @@C:Trm ) ( ( '@server-ts { 0 } ) @@S:Trm )
    ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , @@X:Trm ) , ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kC:Trm ) ) $@& ( $@& (
    ( ( '@shK-msg { 0 } ) @@AKey:Trm ) , ( ( '@nonce-msg { 0 } ) @@n1:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0
    } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( (
    'T_clientASE_resp { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( ( ( @@L:Trm @@C:Trm ) @@T:Trm ) @@n1:Trm ) ) =>
                $union ( ( ( 'F { 0 } ) @fresh':Trm ) , ( ( ( ( ( '@Auth { 0 } ) @@C:Trm ) @@X:Trm ) @@T:Trm ) @@AKey:Trm )
    )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , @@Y:Trm ) , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) $@& ( $@&
    ( ( ( '@shK-msg { 0 } ) @@SKey:Trm ) , ( ( '@nonce-msg { 0 } ) @@n2:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ {
    0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( (
    'T_clientTGE_resp { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( ( ( ( @@L:Trm @@C:Trm ) @@S:Trm ) @@T:Trm ) @@n2:Trm ) ) =>
                $union ( ( ( 'F { 0 } ) @fresh':Trm ) , ( ( ( ( ( '@Service { 0 } ) @@C:Trm ) @@Y:Trm ) @@S:Trm )
    @@SKey:Trm ) )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts
    { 0 } ) @@T:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 } ) @@n1:Trm ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'EL { 0 } )
    ( ( '@dbK { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) @@kC:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( (
    '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) ) ) @@kT:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kT:Trm ) ) $@& ( ( ( '@shK-msg { 0
    } ) @@AKey:Trm ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) ) , ( ( (
    '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kC:Trm ) ) $@& ( $@& ( ( ( '@shK-msg { 0 } ) @@AKey:Trm ) , ( ( '@nonce-msg {
    0 } ) @@n1:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm
    ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm
    ) ) ) @@kC:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) ) )
    @@kT:Trm ) )
                if      @@AKey:Trm := ( ( ( 'FRESH { 0 } ) ( ( ( '@shK { 0 } ) @@C:Trm ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) )
    @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kS:Trm ) )
    @@X:Trm ) , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@SKey:Trm ) ) $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ
    { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( '@time-msg { 0 } ) @@t:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm )
    ) , ( ( 'T_serverCSE_answer { 0 } ) @@S:Trm ) ) , ( ( ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@SKey:Trm ) ) ( (
    '@time-msg { 0 } ) @@t:Trm ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm ) )
    , ( ( ( ( ( '@Mem { 0 } ) @@S:Trm ) @@C:Trm ) @@SKey:Trm ) @@t:Trm ) )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@SKey:Trm ) ) ( (
    '@time-msg { 0 } ) @@t:Trm ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'T_clientCSE_resp { 0 } ) @@C:Trm ) @@L:Trm )
    ) , ( ( ( ( ( @@L:Trm @@C:Trm ) @@S:Trm ) @@SKey:Trm ) @@t:Trm ) @@Y:Trm ) ) =>
                $union ( ( ( 'F { 0 } ) @fresh':Trm ) , ( ( ( ( '@DoneMut { 0 } ) @@C:Trm ) @@S:Trm ) @@SKey:Trm ) )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( $union ( ( ( '@START-CSE { 0 } ) @@C:Trm ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( (
    'T_clientCSE_req { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( ( ( ( ( '@Service { 0 } ) @@C:Trm ) @@Y:Trm ) @@S:Trm ) @@SKey:Trm )
    ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( @@Y:Trm , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } )
    @@SKey:Trm ) ) $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( (
    '@time-msg { 0 } ) @@t:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( ( ( '@Service { 0 } ) @@C:Trm ) @@Y:Trm )
    @@S:Trm ) @@SKey:Trm ) ) , ( ( ( ( ( @@L:Trm @@C:Trm ) @@S:Trm ) @@SKey:Trm ) @@t:Trm ) @@Y:Trm ) )
                if      @@t:Trm := ( ( ( 'FRESH { 0 } ) ( '@time { 0 } ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( $union ( ( ( '@START-TGE { 0 } ) @@C:Trm ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'EL {
    0 } ) ( '@server { 0 } ) ) @@S:Trm ) ) , ( ( ( ( ( '@Auth { 0 } ) @@C:Trm ) @@X:Trm ) @@T:Trm ) @@AKey:Trm ) ) =>
                $union ( $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( @@X:Trm , ( ( (
    '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs
    { 0 } ) @@C:Trm ) ) ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ,
    ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) ) ) ) , ( (
    '@nonce-msg { 0 } ) @@n2:Trm ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm )
    ) , ( ( ( 'T_clientTGE_resp { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( ( ( ( ( '@Auth { 0 } ) @@C:Trm ) @@X:Trm ) @@T:Trm )
    @@AKey:Trm ) ) , ( ( ( ( @@L:Trm @@C:Trm ) @@S:Trm ) @@T:Trm ) @@n2:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '_ : ( '@client { 0 } ) } ( { '_ : ( '@server { 0 } ) } ( { '_
    : ( '@TGS { 0 } ) } ( { '_ : ( '@nonce { 0 } ) } ( '@state { 0 } ) ) ) ) ) ) @fresh:Trm ) /\
                        @@n2:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) ( ( 'suc { 0 } ) @fresh:Trm ) ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm ) ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } )
    @@kT:Trm ) ) $@& ( ( ( '@shK-msg { 0 } ) @@AKey:Trm ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) ( ( '@princ-msg {
    0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0
    } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( (
    '@server-ts { 0 } ) @@S:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 } ) @@n2:Trm ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( (
    'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) ) ) @@kS:Trm ) ) =>
                $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kS:Trm ) ) $@& ( ( ( '@shK-msg { 0
    } ) @@SKey:Trm ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) ) ) ) , ( ( (
    '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) $@& ( $@& ( ( ( '@shK-msg { 0 } ) @@SKey:Trm ) , ( ( '@nonce-msg
    { 0 } ) @@n2:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } )
    @@S:Trm ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( ( '@dbK { 0 } ) ( ( '@ts-tcs { 0 } ) ( (
    '@server-ts { 0 } ) @@S:Trm ) ) ) ) @@kS:Trm ) )
                if      @@SKey:Trm := ( ( ( 'FRESH { 0 } ) ( ( ( '@shK { 0 } ) @@C:Trm ) ( ( '@server-ts { 0 } ) @@S:Trm )
    ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , @@X:Trm ) , ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kC:Trm ) ) $@& ( $@& (
    ( ( '@shK-msg { 0 } ) @@AKey:Trm ) , ( ( '@nonce-msg { 0 } ) @@n1:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0
    } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts { 0 } ) @@T:Trm ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( @@L:Trm
    @@C:Trm ) @@T:Trm ) @@n1:Trm ) ) =>
                $union ( $union ( ( ( 'F { 0 } ) @fresh':Trm ) , ( ( ( 'T_clientASE_req { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( (
    ( ( ( '@Auth { 0 } ) @@C:Trm ) @@X:Trm ) @@T:Trm ) @@AKey:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '_ : ( '@client { 0 } ) } ( { '_ : ( '@TGS { 0 } ) } ( { '_ : (
    '@nonce { 0 } ) } ( '@state { 0 } ) ) ) ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , @@Y:Trm ) , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@AKey:Trm ) ) $@& ( $@&
    ( ( ( '@shK-msg { 0 } ) @@SKey:Trm ) , ( ( '@nonce-msg { 0 } ) @@n2:Trm ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ {
    0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) ) ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( (
    @@L:Trm @@C:Trm ) @@S:Trm ) @@T:Trm ) @@n2:Trm ) ) =>
                $union ( $union ( ( ( 'F { 0 } ) @fresh':Trm ) , ( ( ( 'T_clientTGE_req { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( (
    ( ( ( '@Service { 0 } ) @@C:Trm ) @@Y:Trm ) @@S:Trm ) @@SKey:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '_ : ( '@client { 0 } ) } ( { '_ : ( '@server { 0 } ) } ( { '_
    : ( '@TGS { 0 } ) } ( { '_ : ( '@nonce { 0 } ) } ( '@state { 0 } ) ) ) ) ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( ( ( ( '@encrypt { 0 } ) ( ( '@dbK-key { 0 } ) @@kS:Trm ) ) @@X:Trm
    ) , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@SKey:Trm ) ) $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } )
    ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( '@time-msg { 0 } ) @@t:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( (
    ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@SKey:Trm ) ) ( (
    '@time-msg { 0 } ) @@t:Trm ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'EL { 0 } ) ( '@server { 0 } ) ) @@S:Trm ) )
    , ( ( ( ( ( '@Mem { 0 } ) @@S:Trm ) @@C:Trm ) @@SKey:Trm ) @@t:Trm ) )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( ( ( '@N { 0 } ) ( ( ( '@encrypt { 0 } ) ( ( '@shK-key { 0 } ) @@SKey:Trm ) ) ( (
    '@time-msg { 0 } ) @@t:Trm ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( ( ( @@L:Trm @@C:Trm ) @@S:Trm ) @@SKey:Trm )
    @@t:Trm ) @@Y:Trm ) ) =>
                $union ( $union ( ( ( 'F { 0 } ) @fresh':Trm ) , ( ( ( 'T_clientCSE_req { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( (
    ( ( '@DoneMut { 0 } ) @@C:Trm ) @@S:Trm ) @@SKey:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '@C : ( '@client { 0 } ) } ( { '@S : ( '@server { 0 } ) } ( {
    '_ : ( ( ( '@shK { 0 } ) @@C:Trm ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) } ( { '_ : ( '@time { 0 } ) } ( { '_ : ( '@msg {
    0 } ) } ( '@state { 0 } ) ) ) ) ) ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@START-CSE { 0 } ) @@C:Trm ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( ( ( '@Service {
    0 } ) @@C:Trm ) @@Y:Trm ) @@S:Trm ) @@SKey:Trm ) ) =>
                $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( @@Y:Trm , ( ( ( '@encrypt { 0 } ) ( ( '@shK-key {
    0 } ) @@SKey:Trm ) ) $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( (
    '@time-msg { 0 } ) @@t:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'T_clientCSE_resp { 0 } ) @@C:Trm )
    @@L:Trm ) ) , ( ( ( ( ( '@Service { 0 } ) @@C:Trm ) @@Y:Trm ) @@S:Trm ) @@SKey:Trm ) ) , ( ( ( ( ( @@L:Trm @@C:Trm )
    @@S:Trm ) @@SKey:Trm ) @@t:Trm ) @@Y:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '@C : ( '@client { 0 } ) } ( { '@S : ( '@server { 0 } ) } ( {
    '_ : ( ( ( '@shK { 0 } ) @@C:Trm ) ( ( '@server-ts { 0 } ) @@S:Trm ) ) } ( { '_ : ( '@time { 0 } ) } ( { '_ : ( '@msg {
    0 } ) } ( '@state { 0 } ) ) ) ) ) ) ) @fresh:Trm ) /\
                        @@t:Trm := ( ( ( 'FRESH { 0 } ) ( '@time { 0 } ) ) ( ( 'suc { 0 } ) @fresh:Trm ) ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm ) ) .
        crl     $union ( $union ( ( ( 'F { 0 } ) @fresh:Trm ) , ( ( ( '@START-ASE { 0 } ) @@C:Trm ) @@T:Trm ) ) , ( ( (
    'T_clientASE_req { 0 } ) @@C:Trm ) @@L:Trm ) ) =>
                $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts
    { 0 } ) @@T:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 } ) @@n1:Trm ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( @@L:Trm
    @@C:Trm ) @@T:Trm ) @@n1:Trm ) )
                if      @@n1:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( ( ( 'F { 0 } ) @fresh:Trm ) , ( ( ( '@START-ASE { 0 } ) @@C:Trm ) @@T:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( (
    '@client-tcs { 0 } ) @@C:Trm ) ) ) , ( ( '@princ-msg { 0 } ) ( ( '@tcs-princ { 0 } ) ( ( '@ts-tcs { 0 } ) ( ( '@TGS-ts
    { 0 } ) @@T:Trm ) ) ) ) ) , ( ( '@nonce-msg { 0 } ) @@n1:Trm ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( (
    'T_clientASE_resp { 0 } ) @@C:Trm ) @@L:Trm ) ) , ( ( ( @@L:Trm @@C:Trm ) @@T:Trm ) @@n1:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '_ : ( '@client { 0 } ) } ( { '_ : ( '@TGS { 0 } ) } ( { '_ : (
    '@nonce { 0 } ) } ( '@state { 0 } ) ) ) ) ) @fresh:Trm ) /\
                        @@n1:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) ( ( 'suc { 0 } ) @fresh:Trm ) ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm ) ) .
endm