(act : Type)
(FRESH : {T : Type}nat -> T)
(@princ : Type)
(@msg : Type)
(@nonce : Type)
(@state : Type)
(@empty : @state)
(union : @state -> @state -> @state)
(@& : @msg -> @msg -> @msg)
(@nonce-msg : @nonce -> @msg)
(@princ-msg : @princ -> @msg)
(@N : @msg -> @state)
(@pubK : @princ -> Type)
(@encrypt : {@A | @princ}(@pubK @A)-> @msg -> @msg)
(@START-1 : @princ -> @princ -> @state)
(@START-2 : @princ -> @state)
(@TERMINATED-1 : @princ -> @state)
(@TERMINATED-2 : @princ -> @state)
(@A : @princ)
(@B : @princ)
(@pkA : @pubK @A)
(@pkB : @pubK @B)
(F : nat -> @state)
(EL : {T : Type}T -> @state)
(union_comm : ||{i,j : @state}((union i j)=(union j i)))
(union_assoc : ||{i,j,k : @state}((union i(union j k))=(union(union i j)k)))
(append_assoc : ||{i,j,k : @msg}((@& i(@& j k))=(@&(@& i j)k)))
(L_initiator_Init1_1 : act)
(L_initiator_Init1_2 : act)
(L_initiator_Init2_1 : act)
(L_initiator_Init2_2 : act)
(T_initiator_Init1 : @princ ->(@princ -> @nonce -> @state)-> @state)
(T_initiator_Init2 : @princ ->(@princ -> @nonce -> @state)-> @state)
(R_initiator_Init1_1 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @state)fresh))->
 (@nA :=(FRESH @nonce(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_initiator_Init1_1]:
 (union(union(F fresh)(EL(@pubK @B)@PKB))(@START-1 @A @B))
  =>
 (union(union(union(F fresh')(T_initiator_Init2 @A @L))(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(
    @encrypt @PKB(@&(@nonce-msg @nA)(@princ-msg @A))))))(@L @B @nA))))
(R_initiator_Init1_2 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {fresh,fresh' : nat}
 (@nA :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_initiator_Init1_2]:
 (union(union(union(F fresh)(T_initiator_Init1 @A @L))(EL(@pubK @B)@PKB))(@START-1 @A @B))
  =>
 (union(union(F fresh')(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@&(@nonce-msg @nA)(
    @princ-msg @A))))))(@L @B @nA))))
(R_initiator_Init2_1 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_initiator_Init2_1]:
 (union(union(F fresh)(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(@encrypt @PKA(@&(@nonce-msg @nA)(
    @nonce-msg @nB))))))(@L @B @nA)))
  =>
 (union(union(union(F fresh')(T_initiator_Init1 @A @L))(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(
    @encrypt @PKB(@nonce-msg @nB)))))(@TERMINATED-1 @A))))
(R_initiator_Init2_2 : !!
 {@A : @princ}
 {@L : @princ -> @nonce -> @state}
 {@B : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_initiator_Init2_2]:
 (union(union(union(F fresh)(T_initiator_Init2 @A @L))(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(
    @encrypt @PKA(@&(@nonce-msg @nA)(@nonce-msg @nB))))))(@L @B @nA)))
  =>
 (union(union(F fresh')(EL(@pubK @B)@PKB))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@nonce-msg @nB)))))(
    @TERMINATED-1 @A))))

(L_responder_Resp1_1 : act)
(L_responder_Resp1_2 : act)
(L_responder_Resp2_1 : act)
(L_responder_Resp2_2 : act)
(T_responder_Resp1 : @princ ->(@princ -> @nonce -> @state)-> @state)
(T_responder_Resp2 : @princ ->(@princ -> @nonce -> @state)-> @state)
(R_responder_Resp1_1 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @state}
 {@A : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @state)fresh))->
 (@nB :=(FRESH @nonce(suc fresh)))->
 (fresh' :=(suc(suc fresh)))->
 [L_responder_Resp1_1]:
 (union(union(F fresh)(EL(@pubK @A)@PKA))(union(@START-2 @B)(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@&(
    @nonce-msg @nA)(@princ-msg @A))))))))
  =>
 (union(union(union(F fresh')(T_responder_Resp2 @B @L))(EL(@pubK @A)@PKA))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(
    @encrypt @PKA(@&(@nonce-msg @nA)(@nonce-msg @nB))))))(@L @A @nB))))
(R_responder_Resp1_2 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @state}
 {@A : @princ}
 {@PKA : @pubK @A}
 {@PKB : @pubK @B}
 {@nA : @nonce}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@nB :=(FRESH @nonce fresh))->
 (fresh' :=(suc fresh))->
 [L_responder_Resp1_2]:
 (union(union(union(F fresh)(T_responder_Resp1 @B @L))(EL(@pubK @A)@PKA))(union(@START-2 @B)(@N(@&(@princ-msg @A)(@&(
    @princ-msg @B)(@encrypt @PKB(@&(@nonce-msg @nA)(@princ-msg @A))))))))
  =>
 (union(union(F fresh')(EL(@pubK @A)@PKA))(union(@N(@&(@princ-msg @B)(@&(@princ-msg @A)(@encrypt @PKA(@&(@nonce-msg @nA)(
    @nonce-msg @nB))))))(@L @A @nB))))
(R_responder_Resp2_1 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @state}
 {@A : @princ}
 {@PKB : @pubK @B}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (@L :=(FRESH(@princ -> @nonce -> @state)fresh))->
 (fresh' :=(suc fresh))->
 [L_responder_Resp2_1]:
 (union(F fresh)(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@nonce-msg @nB)))))(@L @A @nB)))
  =>
 (union(union(F fresh')(T_responder_Resp1 @B @L))(@TERMINATED-2 @B)))
(R_responder_Resp2_2 : !!
 {@B : @princ}
 {@L : @princ -> @nonce -> @state}
 {@A : @princ}
 {@PKB : @pubK @B}
 {@nB : @nonce}
 {fresh,fresh' : nat}
 (fresh' := fresh)->
 [L_responder_Resp2_2]:
 (union(union(F fresh)(T_responder_Resp2 @B @L))(union(@N(@&(@princ-msg @A)(@&(@princ-msg @B)(@encrypt @PKB(@nonce-msg
    @nB)))))(@L @A @nB)))
  =>
 (union(F fresh')(@TERMINATED-2 @B)))

(config :=(union(F 0)(union(union(union(union(EL @princ @A)(EL @princ @B))(EL(@pubK @A)@pkA))(EL(@pubK @B)@pkB))(union(
    @START-1 @A @B)(@START-2 @B)))))
(red config)