Proof

Step	Formula	Justification	Bindings
1	( :_g5 ) list:member :_g5 .	built-in Axiom list:member
2	...	parsing <mashup.n3>
3	@forSome run:_g5 . :Q1 ht:headers ( run:_g5 ) . :bob :cookie "s3lkw3lij4wl3i" . run:_g5 ht:fieldName "Cookie"; ht:fieldValue "s3lkw3lij4wl3i" .	erasure from step 2
4	@forAll :COOKIE, :Q, :USER . { :Q ht:headers [ list:member [ ht:fieldName "Cookie"; ht:fieldValue :COOKIE ] ] . :USER ma:cookie :COOKIE . } log:implies {:Q c:speaks_for :USER . } .	erasure from step 2
5	...	rule from step 4 applied to steps (1, 3)	{'Q': u'<mashup#Q1>', '_g_L89C33': '[...]', 'COOKIE': '"s3lk...wl3i"', 'USER': u'<mashup#bob>', '_g_L89C19': '?'}
6	:Q1 c:speaks_for :bob .	erasure from step 5
7	( "&amount=1000000&for=mallory" "[?&]([^=]+)=([^&]+)(.*)" ) :search ( "amount" "1000000" "&for=mallory" ) .	built-in Axiom str:search
8	( "?account=bob&amount=1000000&for=mallory" "[?&]([^=]+)=([^&]+)(.*)" ) :search ( "account" "bob" "&amount=1000000&for=mallory" ) .	built-in Axiom str:search
9	( "http://bank.example/withdraw?account=bob&amount=1000000&for=mallory" "http:[^?]+(\?.*)" ) :search ( "?account=bob&amount=1000000&for=mallory" ) .	built-in Axiom str:search
10	:Q1 ht:absoluteURI "http://bank.example/withdraw?account=bob&amount=1000000&for=mallory" .	erasure from step 2
11	@forAll :I, :PARAMS, :Q . { ( :I "http:[^?]+(\?.*)" ) str:search ( :PARAMS ) . :Q ht:absoluteURI :I . } log:implies {:Q ma:formParams :PARAMS . } .	erasure from step 2
12	...	rule from step 11 applied to steps (9, 10)	{'I': '"http...lory"', 'Q': u'<mashup#Q1>', 'PARAMS': '"?acc...lory"'}
13	:Q1 :formParams "?account=bob&amount=1000000&for=mallory" .	erasure from step 12
14	@forAll :N, :PARAMS, :Q, :REST, :V . { ( :PARAMS "[?&]([^=]+)=([^&]+)(.*)" ) str:search ( :N :V :REST ) . :Q ma:formParams :PARAMS . } log:implies { @forSome run:_g6 . run:_g6 ma:paramName :N; ma:paramValue :V . :Q ma:formParam run:_g6; ma:formParams :REST . } .	erasure from step 2
15	...	rule from step 14 applied to steps (8, 13)	{'Q': u'<mashup#Q1>', 'N': '"account"', 'PARAMS': '"?acc...lory"', 'REST': '"&amo...lory"', 'V': '"bob"'}
16	:Q1 :formParams "&amount=1000000&for=mallory" .	erasure from step 15
17	@forAll :N, :PARAMS, :Q, :REST, :V . { ( :PARAMS "[?&]([^=]+)=([^&]+)(.*)" ) str:search ( :N :V :REST ) . :Q ma:formParams :PARAMS . } log:implies { @forSome run:_g6 . run:_g6 ma:paramName :N; ma:paramValue :V . :Q ma:formParam run:_g6; ma:formParams :REST . } .	erasure from step 2
18	...	rule from step 17 applied to steps (7, 16)	{'Q': u'<mashup#Q1>', 'N': '"amount"', 'PARAMS': '"&amo...lory"', 'REST': '"&for...lory"', 'V': '"1000000"'}
19	:Q1 :formParam [ :paramName "amount"; :paramValue "1000000" ] .	erasure from step 18
20	:bobAccount :accountName "bob" . :malloryAccount :accountName "mallory" .	erasure from step 2
21	( "&for=mallory" "[?&]([^=]+)=([^&]+)(.*)" ) :search ( "for" "mallory" "" ) .	built-in Axiom str:search
22	:Q1 :formParams "&for=mallory" .	erasure from step 18
23	@forAll :N, :PARAMS, :Q, :REST, :V . { ( :PARAMS "[?&]([^=]+)=([^&]+)(.*)" ) str:search ( :N :V :REST ) . :Q ma:formParams :PARAMS . } log:implies { @forSome run:_g6 . run:_g6 ma:paramName :N; ma:paramValue :V . :Q ma:formParam run:_g6; ma:formParams :REST . } .	erasure from step 2
24	...	rule from step 23 applied to steps (21, 22)	{'Q': u'<mashup#Q1>', 'N': '"for"', 'PARAMS': '"&for...lory"', 'REST': '""', 'V': '"mallory"'}
25	:Q1 :formParam [ :paramName "for"; :paramValue "mallory" ] .	erasure from step 24
26	:Q1 :formParam [ :paramName "account"; :paramValue "bob" ] .	erasure from step 15
27	@forAll :A1, :A2, :AMT, mas:ACCT, mas:FOR, mas:Q . { :A1 :accountName mas:ACCT . :A2 :accountName mas:FOR . mas:Q :formParam [ :paramName "account"; :paramValue mas:ACCT ], [ :paramName "amount"; :paramValue :AMT ], [ :paramName "for"; :paramValue mas:FOR ] . } log:implies {mas:Q c:says {:A1 :debit :AMT . :A2 :credit :AMT . } . } .	erasure from step 2
28	...	rule from step 27 applied to steps (19, 20, 25, 26)	{'A1': u'<mashup#bobAccount>', 'FOR': '"mallory"', '_g_L67C18': '[...]', '_g_L68C18': '[...]', 'Q': u'<mashup#Q1>', 'A2': u'<mashup#malloryAccount>', '_g_L66C18': '[...]', 'ACCT': '"bob"', 'AMT': '"1000000"'}
29	:Q1 c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } .	erasure from step 28
30	...	parsing <speech.n3>
31	@forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } .	erasure from step 30
32	...	rule from step 31 applied to steps (6, 29)	{'A': u'<mashup#Q1>', 's': '{2}', 'B': u'<mashup#bob>'}
33	:bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } .	erasure from step 32
34	...	parsing <xsrf-goal.n3>
35	{ :bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . } log:implies {:bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . } .	erasure from step 34
36	:bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } .	rule from step 35 applied to steps (33,)	{}

Conclusion:

@prefix : <mashup#> .
@prefix c: <speech#> .

:bob     c:says {:bobAccount     :debit "1000000" .
:malloryAccount     :credit "1000000" .
} .