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 } ) ( '@princ { 0 } ) ) ( '@S { 0 } ) ) ) ( ( ( 'EL { 0
    } ) ( '@princ { 0 } ) ) ( '@A { 0 } ) ) ) ) ( ( ( 'EL { 0 } ) ( '@princ { 0 } ) ) ( '@B { 0 } ) ) ) ) ( ( ( 'EL { 0 } )
    ( ( ( '@ltK { 0 } ) ( '@A { 0 } ) ) ( '@S { 0 } ) ) ) ( '@kAS { 0 } ) ) ) ) ( ( ( 'EL { 0 } ) ( ( ( '@ltK { 0 } ) ( '@B
    { 0 } ) ) ( '@S { 0 } ) ) ) ( '@kBS { 0 } ) ) ) ) ( ( ( 'union { 0 } ) ( ( ( '@START-1 { 0 } ) ( '@A { 0 } ) ) ( '@B {
    0 } ) ) ) ( ( ( 'union { 0 } ) ( ( '@START-2 { 0 } ) ( '@B { 0 } ) ) ) ( ( '@START-3 { 0 } ) ( '@S { 0 } ) ) ) ) ) ) .
        crl     $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , (
    ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , @@X:Trm ) ) , ( ( '@START-2 { 0 } ) @@B:Trm )
    ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@B:Trm ) ( '@S { 0 } ) ) ) @@kBS:Trm ) ) , (
    ( ( 'T_responder_Resp1 { 0 } ) @@B:Trm ) @@L:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , @@X:Trm ) , ( ( ( '@encrypt { 0 } ) ( (
    '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@nonce-msg { 0 } ) @@n:Trm
    ) ) , ( ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) )
    , ( ( ( 'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@B:Trm ) ( '@S { 0 } ) ) ) @@kBS:Trm ) ) , ( ( ( ( ( @@L:Trm @@B:Trm ) @@A:Trm
    ) @@n:Trm ) @@nB:Trm ) @@kBS:Trm ) )
                if      @@nB:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , @@X:Trm ) ) , ( ( '@START-2 { 0 } ) @@B:Trm ) )
    , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@B:Trm ) ( '@S { 0 } ) ) ) @@kBS:Trm ) ) =>
                $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm
    ) , ( ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , @@X:Trm ) , ( ( ( '@encrypt { 0 } ) ( (
    '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@nonce-msg { 0 } ) @@n:Trm
    ) ) , ( ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) )
    , ( ( ( 'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@B:Trm ) ( '@S { 0 } ) ) ) @@kBS:Trm ) ) , ( ( ( 'T_responder_Resp2 { 0 } )
    @@B:Trm ) @@L:Trm ) ) , ( ( ( ( ( @@L:Trm @@B:Trm ) @@A:Trm ) @@n:Trm ) @@nB:Trm ) @@kBS:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '@B : ( '@princ { 0 } ) } ( { '_ : ( '@princ { 0 } ) } ( { '_ :
    ( '@nonce { 0 } ) } ( { '_ : ( '@nonce { 0 } ) } ( { '_ : ( ( ( '@ltK { 0 } ) @@B:Trm ) ( '@S { 0 } ) ) } ( '@state { 0
    } ) ) ) ) ) ) ) @fresh:Trm ) /\
                        @@nB:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) ( ( 'suc { 0 } ) @fresh:Trm ) ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm ) ) .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , @@Y:Trm ) , ( (
    ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@stK-msg { 0 }
    ) @@kAB:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'T_responder_Resp2 { 0 } ) @@B:Trm ) @@L:Trm ) ) , ( ( (
    ( ( @@L:Trm @@B:Trm ) @@A:Trm ) @@n:Trm ) @@nB:Trm ) @@kBS:Trm ) ) =>
                $union ( $union ( ( ( '@N { 0 } ) $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , @@Y:Trm ) ) , ( (
    '@TERMINATED-2 { 0 } ) @@B:Trm ) ) , ( ( 'F { 0 } ) @fresh':Trm ) )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( ( ( '@encrypt { 0 }
    ) ( ( '@ltK-shK { 0 } ) @@kAS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@stK-msg { 0 } ) @@kAB:Trm ) ) )
    ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( 'T_initiator_Init2 { 0 } ) @@A:Trm ) @@L:Trm ) ) , ( ( ( ( @@L:Trm @@A:Trm
    ) @@B:Trm ) @@n:Trm ) @@nA:Trm ) ) =>
                $union ( ( ( '@TERMINATED-1 { 0 } ) @@A:Trm ) , ( ( 'F { 0 } ) @fresh':Trm ) )
                if      @fresh':Trm := @fresh:Trm .
        crl     $union ( $union ( $union ( ( ( 'F { 0 } ) @fresh:Trm ) , ( ( ( '@START-1 { 0 } ) @@A:Trm ) @@B:Trm ) ) , (
    ( ( 'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@A:Trm ) ( '@S { 0 } ) ) ) @@kAS:Trm ) ) , ( ( ( 'T_initiator_Init1 { 0 } )
    @@A:Trm ) @@L:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } )
    @@kAS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@nonce-msg { 0 } ) @@n:Trm ) ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( (
    'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@A:Trm ) ( '@S { 0 } ) ) ) @@kAS:Trm ) ) , ( ( ( ( @@L:Trm @@A:Trm ) @@B:Trm ) @@n:Trm
    ) @@nA:Trm ) )
                if      @@n:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) @fresh:Trm ) /\
                        @@nA:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) ( ( 'suc { 0 } ) @fresh:Trm ) ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm ) ) .
        crl     $union ( $union ( $union ( ( 'T_server_Server1 { 0 } ) , ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( ( (
    '@nonce-msg { 0 } ) @@n:Trm ) , ( ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , ( ( (
    '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } ) @@kAS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( (
    '@nonce-msg { 0 } ) @@n:Trm ) ) , ( ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) , ( ( (
    '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( (
    '@nonce-msg { 0 } ) @@n:Trm ) ) , ( ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) ) ) , (
    ( '@START-3 { 0 } ) ( '@S { 0 } ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) =>
                $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( ( ( '@encrypt { 0 } ) (
    ( '@ltK-shK { 0 } ) @@kAS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@stK-msg { 0 } ) @@kAB:Trm ) ) ) ) ,
    ( ( ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@stK-msg {
    0 } ) @@kAB:Trm ) ) ) ) ) , ( ( '@TERMINATED-3 { 0 } ) ( '@S { 0 } ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) )
                if      @@kAB:Trm := ( ( ( 'FRESH { 0 } ) ( ( ( '@stK { 0 } ) @@A:Trm ) @@B:Trm ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } )
    @@kAS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@nonce-msg { 0 } ) @@n:Trm ) ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 }
    ) @@kBS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@nonce-msg { 0 } ) @@n:Trm ) ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) ) , ( ( '@START-3 { 0 } ) ( '@S { 0 } ) ) ) ,
    ( ( 'F { 0 } ) @fresh:Trm ) ) =>
                $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( ( ( '@encrypt { 0 } ) (
    ( '@ltK-shK { 0 } ) @@kAS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@stK-msg { 0 } ) @@kAB:Trm ) ) ) ) ,
    ( ( ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@stK-msg {
    0 } ) @@kAB:Trm ) ) ) ) ) , ( ( '@TERMINATED-3 { 0 } ) ( '@S { 0 } ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) )
                if      @@kAB:Trm := ( ( ( 'FRESH { 0 } ) ( ( ( '@stK { 0 } ) @@A:Trm ) @@B:Trm ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , @@Y:Trm ) , ( ( (
    '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } ) @@kBS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nB:Trm ) , ( ( '@stK-msg { 0 } )
    @@kAB:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( ( ( @@L:Trm @@B:Trm ) @@A:Trm ) @@n:Trm ) @@nB:Trm )
    @@kBS:Trm ) ) =>
                $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , @@Y:Trm ) ) , ( (
    '@TERMINATED-2 { 0 } ) @@B:Trm ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( ( 'T_responder_Resp1 { 0 } ) @@B:Trm )
    @@L:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '@B : ( '@princ { 0 } ) } ( { '_ : ( '@princ { 0 } ) } ( { '_ :
    ( '@nonce { 0 } ) } ( { '_ : ( '@nonce { 0 } ) } ( { '_ : ( ( ( '@ltK { 0 } ) @@B:Trm ) ( '@S { 0 } ) ) } ( '@state { 0
    } ) ) ) ) ) ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( '@N { 0 } ) $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , ( ( ( '@encrypt { 0 } ) ( (
    '@ltK-shK { 0 } ) @@kAS:Trm ) ) $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@stK-msg { 0 } ) @@kAB:Trm ) ) ) ) ) ,
    ( ( 'F { 0 } ) @fresh:Trm ) ) , ( ( ( ( @@L:Trm @@A:Trm ) @@B:Trm ) @@n:Trm ) @@nA:Trm ) ) =>
                $union ( $union ( ( ( '@TERMINATED-1 { 0 } ) @@A:Trm ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( (
    'T_initiator_Init1 { 0 } ) @@A:Trm ) @@L:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '_ : ( '@princ { 0 } ) } ( { '_ : ( '@princ { 0 } ) } ( { '_ :
    ( '@nonce { 0 } ) } ( { '_ : ( '@nonce { 0 } ) } ( '@state { 0 } ) ) ) ) ) ) @fresh:Trm ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) @fresh:Trm ) .
        crl     $union ( $union ( ( ( 'F { 0 } ) @fresh:Trm ) , ( ( ( '@START-1 { 0 } ) @@A:Trm ) @@B:Trm ) ) , ( ( ( 'EL {
    0 } ) ( ( ( '@ltK { 0 } ) @@A:Trm ) ( '@S { 0 } ) ) ) @@kAS:Trm ) ) =>
                $union ( $union ( $union ( $union ( ( ( '@N { 0 } ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@n:Trm ) , (
    ( '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) , ( ( ( '@encrypt { 0 } ) ( ( '@ltK-shK { 0 } )
    @@kAS:Trm ) ) $@& ( $@& ( $@& ( ( ( '@nonce-msg { 0 } ) @@nA:Trm ) , ( ( '@nonce-msg { 0 } ) @@n:Trm ) ) , ( (
    '@princ-msg { 0 } ) @@A:Trm ) ) , ( ( '@princ-msg { 0 } ) @@B:Trm ) ) ) ) ) , ( ( 'F { 0 } ) @fresh':Trm ) ) , ( ( (
    'EL { 0 } ) ( ( ( '@ltK { 0 } ) @@A:Trm ) ( '@S { 0 } ) ) ) @@kAS:Trm ) ) , ( ( ( 'T_initiator_Init2 { 0 } ) @@A:Trm )
    @@L:Trm ) ) , ( ( ( ( @@L:Trm @@A:Trm ) @@B:Trm ) @@n:Trm ) @@nA:Trm ) )
                if      @@L:Trm := ( ( ( 'FRESH { 0 } ) ( { '_ : ( '@princ { 0 } ) } ( { '_ : ( '@princ { 0 } ) } ( { '_ :
    ( '@nonce { 0 } ) } ( { '_ : ( '@nonce { 0 } ) } ( '@state { 0 } ) ) ) ) ) ) @fresh:Trm ) /\
                        @@n:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) ( ( 'suc { 0 } ) @fresh:Trm ) ) /\
                        @@nA:Trm := ( ( ( 'FRESH { 0 } ) ( '@nonce { 0 } ) ) ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm )
    ) ) /\
                        @fresh':Trm := ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) ( ( 'suc { 0 } ) @fresh:Trm ) ) ) .
endm