equal
deleted
inserted
replaced
98 inductive "synth H" |
98 inductive "synth H" |
99 intrs |
99 intrs |
100 Inj "X: H ==> X: synth H" |
100 Inj "X: H ==> X: synth H" |
101 Agent "Agent agt : synth H" |
101 Agent "Agent agt : synth H" |
102 MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" |
102 MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" |
103 Crypt "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H" |
103 Crypt "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H" |
104 |
104 |
105 end |
105 end |