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" .
} .
```